diff options
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/MExtraction.v | 17 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 23 | ||||
| -rw-r--r-- | plugins/micromega/persistent_cache.ml | 4 |
3 files changed, 22 insertions, 22 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index e5b5854f0a..362cc3a597 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -49,16 +49,13 @@ Extract Constant Rmult => "( * )". Extract Constant Ropp => "fun x -> - x". Extract Constant Rinv => "fun x -> 1 / x". -(** We now extract to stdout, see comment in Makefile.build *) - -(*Extraction "plugins/micromega/micromega.ml" *) -Recursive Extraction - List.map simpl_cone (*map_cone indexes*) - denorm Qpower vm_add - n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. - - - +(** In order to avoid annoying build dependencies the actual + extraction is only performed as a test in the test suite. *) +(* Extraction "plugins/micromega/micromega.ml" *) +(* Recursive Extraction *) +(* List.map simpl_cone (*map_cone indexes*) *) +(* denorm Qpower vm_add *) +(* n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. *) (* Local Variables: *) (* coding: utf-8 *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 218342efe4..cb54cac3f1 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -984,7 +984,9 @@ struct let parse_expr sigma parse_constant parse_exp ops_spec env term = if debug - then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term); + then ( + let _, env = Pfedit.get_current_context () in + Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term)); (* let constant_or_variable env term = @@ -1103,9 +1105,10 @@ struct | _ -> raise ParseError - let rconstant sigma term = + let rconstant sigma term = + let _, env = Pfedit.get_current_context () in if debug - then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ()); + then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ()); let res = rconstant sigma term in if debug then (Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ; @@ -1145,9 +1148,9 @@ struct let parse_arith parse_op parse_expr env cstr gl = let sigma = gl.sigma in - if debug - then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); - match EConstr.kind sigma cstr with + if debug + then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ()); + match EConstr.kind sigma cstr with | Term.App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr sigma env lhs in @@ -1908,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in - Feedback.msg_notice (Printer.pr_leconstr ff); + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff); Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff end; @@ -1932,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 Feedback.msg_notice (Pp.str "\nAFormula\n") ; let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ - (dump_cstr spec.typ spec.dump_coeff) ff' in - Feedback.msg_notice (Printer.pr_leconstr ff'); - Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' + (dump_cstr spec.typ spec.dump_coeff) ff' in + Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff'); + Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff' end; (* Even if it does not work, this does not mean it is not provable diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 49ccb468c1..387a525141 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -149,7 +149,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.add htbl key elem ; + Table.replace htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -195,7 +195,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.add tbl k e ; + Table.replace tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; |