aboutsummaryrefslogtreecommitdiff
path: root/plugins/micromega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/Lia.v2
-rw-r--r--plugins/micromega/Psatz.v2
-rw-r--r--plugins/micromega/QMicromega.v2
-rw-r--r--plugins/micromega/RMicromega.v2
-rw-r--r--plugins/micromega/RingMicromega.v2
-rw-r--r--plugins/micromega/ZMicromega.v2
-rw-r--r--plugins/micromega/coq_micromega.ml32
-rw-r--r--plugins/micromega/g_micromega.ml45
-rw-r--r--plugins/micromega/persistent_cache.ml8
9 files changed, 26 insertions, 31 deletions
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 3e58e81ac2..52bf5ed3df 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -16,7 +16,7 @@ Require Import ZMicromega.
Require Import ZArith.
Require Import RingMicromega.
Require Import VarMap.
-Require Tauto.
+Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
Ltac preprocess :=
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index ba1f8956e3..fafd8a5f21 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -20,7 +20,7 @@ Require Import ZArith.
Require Import Rdefinitions.
Require Import RingMicromega.
Require Import VarMap.
-Require Tauto.
+Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
Ltac preprocess :=
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index 432683635f..b13285f537 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -168,7 +168,7 @@ Proof.
exact H.
Qed.
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 72353a99e5..2352d78d63 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -533,7 +533,7 @@ Proof.
exact H.
Qed.
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool.
Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 751a81df12..ed49c3df43 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -794,7 +794,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) :=
| OpLe => (psub lhs rhs ,Strict) :: nil
end.
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
Definition cnf_normalise (t:Formula C) : cnf (NFormula) :=
List.map (fun x => x::nil) (xnormalise t).
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index d7ddef2be4..5aa8d03f99 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -198,7 +198,7 @@ Definition xnormalise (t:Formula Z) : list (NFormula Z) :=
| OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
end.
-Require Import Tauto BinNums.
+Require Import Coq.micromega.Tauto BinNums.
Definition normalise (t:Formula Z) : cnf (NFormula Z) :=
List.map (fun x => x::nil) (xnormalise t).
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5fef6d3fc6..e4aa1448eb 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -18,9 +18,7 @@
open Pp
open Mutils
-open Proofview
open Goptions
-open Proofview.Notations
(**
* Debug flag
@@ -963,7 +961,7 @@ struct
let parse_expr parse_constant parse_exp ops_spec env term =
if debug
- then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
+ then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
(*
let constant_or_variable env term =
@@ -1084,7 +1082,7 @@ struct
let rconstant term =
if debug
- then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
+ then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
let res = rconstant term in
if debug then
(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1124,7 +1122,7 @@ struct
let parse_arith parse_op parse_expr env cstr gl =
if debug
- then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
+ then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm cstr ++ fnl ());
match kind_of_term cstr with
| App(op,args) ->
let (op,lhs,rhs) = parse_op gl (op,args) in
@@ -1466,7 +1464,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*
]
(Tacmach.pf_concl gl))
;
- Tactics.new_generalize env ;
+ Tactics.generalize env ;
Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)
]
end }
@@ -1653,12 +1651,12 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
if debug then
begin
- Pp.pp (Pp.str "Formula....\n") ;
+ Feedback.msg_notice (Pp.str "Formula....\n") ;
let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
let ff = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff in
- Pp.pp (Printer.prterm ff) ; Pp.pp_flush ();
- Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
+ Feedback.msg_notice (Printer.prterm ff);
+ Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
end;
match witness_list_tags prover cnf_ff with
@@ -1678,11 +1676,11 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
if debug then
begin
- Pp.pp (Pp.str "\nAFormula\n") ;
+ Feedback.msg_notice (Pp.str "\nAFormula\n") ;
let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
let ff' = dump_formula formula_typ
(dump_cstr spec.typ spec.dump_coeff) ff' in
- Pp.pp (Printer.prterm ff') ; Pp.pp_flush ();
+ Feedback.msg_notice (Printer.prterm ff');
Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
end;
@@ -1728,14 +1726,14 @@ let micromega_gen
| Some (ids,ff',res') ->
(Tacticals.New.tclTHENLIST
[
- Tactics.new_generalize (List.map Term.mkVar ids) ;
+ Tactics.generalize (List.map Term.mkVar ids) ;
micromega_order_change spec res'
(Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
])
with
| ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
| Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
- | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+ | CsdpNotFound -> flush stdout ;
Tacticals.New.tclFAIL 0 (Pp.str
(" Skipping what remains of this tactic: the complexity of the goal requires "
^ "the use of a specialized external tool called csdp. \n\n"
@@ -1776,7 +1774,7 @@ let micromega_order_changer cert env ff =
("__wit", cert, cert_typ)
]
(Tacmach.pf_concl gl)));
- Tactics.new_generalize env ;
+ Tactics.generalize env ;
Tacticals.New.tclTHENLIST (List.map (fun id -> (Tactics.introduction id)) ids)
]
end }
@@ -1814,13 +1812,13 @@ let micromega_genr prover =
(List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
(Tacticals.New.tclTHENLIST
[
- Tactics.new_generalize (List.map Term.mkVar ids) ;
+ Tactics.generalize (List.map Term.mkVar ids) ;
micromega_order_changer res' env (abstract_wrt_formula ff' ff)
])
with
| Mfourier.TimeOut -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut")
| ParseError -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
- | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+ | CsdpNotFound ->
Tacticals.New.tclFAIL 0 (Pp.str
(" Skipping what remains of this tactic: the complexity of the goal requires "
^ "the use of a specialized external tool called csdp. \n\n"
@@ -1905,7 +1903,7 @@ let call_csdpcert_q provername poly =
let cert = Certificate.q_cert_of_pos cert in
if Mc.qWeakChecker poly cert
then Some cert
- else ((print_string "buggy certificate" ; flush stdout) ;None)
+ else ((print_string "buggy certificate") ;None)
let call_csdpcert_z provername poly =
let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index bca1c2febd..e6b5cc60d4 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,12 +16,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Errors
-open Misctypes
-open Stdarg
open Constrarg
-open Pcoq.Prim
-open Pcoq.Tactic
DECLARE PLUGIN "micromega_plugin"
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 6a03e2d61f..88b13abf9a 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -212,9 +212,11 @@ let find t k =
res
let memo cache f =
- let tbl = lazy (open_in cache) in
- fun x ->
- let tbl = Lazy.force tbl in
+ let tbl = lazy (try Some (open_in cache) with _ -> None) in
+ fun x ->
+ match Lazy.force tbl with
+ | None -> f x
+ | Some tbl ->
try
find tbl x
with
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 14:32:08 +0000