Commit 064e4df3 authored by Andrei Paskevich's avatar Andrei Paskevich

coq-tactics: load Why3 plugins

parent 64f07c3e
......@@ -780,12 +780,6 @@ src/coq-tactic/.why3-vo-opt: lib/coq-tactic/Why3.v lib/coq-tactic/why3tac.cmxs
WHY3CONFIG="" $(COQC) -opt -I lib/coq-tactic/ $< && \
touch src/coq-tactic/.why3-vo-opt
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
$(COQC) -byte -I lib/coq-tactic/ src/coq-tactic/test.v
test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
$(COQC) -opt -I lib/coq-tactic/ src/coq-tactic/test.v
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
......@@ -1205,7 +1199,11 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa
printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2)
@rm -f test-session.opt why3session.xml
test-coq-tactic.byte: src/coq-tactic/.why3-vo-byte
$(COQC) -byte -I lib/coq-tactic/ bench/coq-tactic/test.v
test-coq-tactic.opt: src/coq-tactic/.why3-vo-opt
$(COQC) -opt -I lib/coq-tactic/ bench/coq-tactic/test.v
#only test the compilation of runstrat
test-runstrat.byte: lib/why3/why3.cma lib/why3/META
......
......@@ -1177,12 +1177,19 @@ let tr_top_decls () =
let pr_fp fp =
pr_str (Pp.string_of_wnl Whyconf.print_filter_prover fp)
let plugins_loaded = ref false
let why3tac ?(timelimit=timelimit) s gl =
(* print_dep Format.err_formatter; *)
let concl_type = pf_type_of gl (pf_concl gl) in
if not (is_Prop concl_type) then error "Conclusion is not a Prop";
task := Task.use_export None Theory.builtin_theory;
try
(* OCaml doesn't let us do it at the initialisation time *)
if not !plugins_loaded then begin
Whyconf.load_plugins main;
plugins_loaded := true
end;
(* add global declarations from modules Top and Why3.X.Y *)
tr_top_decls ();
(* then translate the goal *)
......
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