Commit 7c6ac4b5 authored by Claude Marche's avatar Claude Marche

fix plugins install : clean old plugins

parent 164f2bc9
......@@ -366,6 +366,7 @@ clean::
rm -f lib/plugins/*
install_no_local::
rm -rf $(LIBDIR)/why3/plugins
mkdir -p $(LIBDIR)/why3/plugins
cp -f $(foreach f,$(LIBPLUGCMO) $(LIBPLUGCMXS),$(wildcard $(f))) $(LIBDIR)/why3/plugins
......
......@@ -137,6 +137,7 @@ New features:
o dropped support for Coq 8.2
o new scheme for Coq realizations using type classes
o Support for PVS 6.0, including realizations
o support for iProver and Zenon
o a warning is emitted for unused bound logic variables in
"forall", "exists" and "let"
......
......@@ -246,7 +246,7 @@ and comment_line = parse
{ comment_line lexbuf }
{
(* dead code
let with_location f lb =
if Debug.test_flag Debug.stack_trace then f lb else
try f lb with
......@@ -259,9 +259,9 @@ and comment_line = parse
let ast = with_location (tptp_file token) lb in
(), Tptp_typing.typecheck env path ast
let library_of_env = Env.register_format "tptp" ["p";"ax"] read_channel
let _library_of_env = Env.register_format "tptp" ["p";"ax"] read_channel
~desc:"TPTP format (CNF FOF FOFX TFF)"
*)
}
(*
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment