Imported Upstream version 8.6upstream/8.6

5 files changed, 48 insertions, 38 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index b84cf254..187601fc 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1074,16 +1074,19 @@ Qed.
    avait utilisé le test précédent et fait une elimination dessus. *)
 
 Ltac elim_eq_term t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (eq_term t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (eq_term_true t1 t2 Aux); clear Aux
    | generalize (eq_term_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_beq t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (beq t1 t2); apply bool_eq_ind; intro Aux;
    [ generalize (beq_true t1 t2 Aux); clear Aux
    | generalize (beq_false t1 t2 Aux); clear Aux ].
 
 Ltac elim_bgt t1 t2 :=
+  let Aux := fresh "Aux" in
   pattern (bgt t1 t2); apply bool_eq_ind; intro Aux;
   [ generalize (bgt_true t1 t2 Aux); clear Aux
   | generalize (bgt_false t1 t2 Aux); clear Aux ].
@@ -1448,27 +1451,27 @@ Ltac loop t :=
   | (Tint ?X1) => loop X1
   (* Eliminations *)
   | match ?X1 with
-    | EqTerm x x0 => _
-    | LeqTerm x x0 => _
+    | EqTerm _ _ => _
+    | LeqTerm _ _ => _
     | TrueTerm => _
     | FalseTerm => _
-    | Tnot x => _
-    | GeqTerm x x0 => _
-    | GtTerm x x0 => _
-    | LtTerm x x0 => _
-    | NeqTerm x x0 => _
-    | Tor x x0 => _
-    | Tand x x0 => _
-    | Timp x x0 => _
-    | Tprop x => _
+    | Tnot _ => _
+    | GeqTerm _ _ => _
+    | GtTerm _ _ => _
+    | LtTerm _ _ => _
+    | NeqTerm _ _ => _
+    | Tor _ _ => _
+    | Tand _ _ => _
+    | Timp _ _ => _
+    | Tprop _ => _
     end => destruct X1; auto; Simplify
   | match ?X1 with
-    | Tint x => _
-    | (x + x0)%term => _
-    | (x * x0)%term => _
-    | (x - x0)%term => _
-    | (- x)%term => _
-    | [x]%term => _
+    | Tint _ => _
+    | (_ + _)%term => _
+    | (_ * _)%term => _
+    | (_ - _)%term => _
+    | (- _)%term => _
+    | [_]%term => _
     end => destruct X1; auto; Simplify
   | (if beq ?X1 ?X2 then _ else _) =>
       let H := fresh "H" in
@@ -1492,7 +1495,7 @@ with Simplify := match goal with
   end.
 
 Ltac prove_stable x th :=
-  match constr:x with
+  match constr:(x) with
   | ?X1 =>
       unfold term_stable, X1; intros; Simplify; simpl;
        apply th
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 21b0f78b..4935fe4b 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -39,7 +39,7 @@ let destructurate t =
     | Term.Var id,[] -> Kvar(Names.Id.to_string id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
-	Errors.error "Omega: Not a quantifier-free goal"
+	CErrors.error "Omega: Not a quantifier-free goal"
     | _ -> Kufo
 
 exception Destruct
@@ -346,7 +346,7 @@ let parse_term t =
     | Kapp("Z.succ",[t]) -> Tsucc t
     | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
-	(try Tnum (recognize t) with e when Errors.noncritical e -> Tother)
+	(try Tnum (recognize t) with e when CErrors.noncritical e -> Tother)
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
 
@@ -368,6 +368,6 @@ let is_scalar t =
     | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
     | _ -> false in
-  try aux t with e when Errors.noncritical e -> false
+  try aux t with e when CErrors.noncritical e -> false
 
 end
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 0a99a26b..830dc54d 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,16 +10,24 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Names
 open Refl_omega
+open Constrarg
+
+let eval_tactic name =
+  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
+  let kn = KerName.make2 (MPfile dp) (Label.make name) in
+  let tac = Tacenv.interp_ltac kn in
+  Tacinterp.eval_tactic tac
 
 let romega_tactic l =
   let tacs = List.map
     (function
-       | "nat" -> Tacinterp.interp <:tactic<zify_nat>>
-       | "positive" -> Tacinterp.interp <:tactic<zify_positive>>
-       | "N" -> Tacinterp.interp <:tactic<zify_N>>
-       | "Z" -> Tacinterp.interp <:tactic<zify_op>>
-       | s -> Errors.error ("No ROmega knowledge base for type "^s))
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
+       | s -> CErrors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
   Tacticals.New.tclTHEN
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 560e6a89..ba882e39 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -9,7 +9,7 @@
 open Pp
 open Util
 open Const_omega
-module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
+module OmegaSolver = Omega_plugin.Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
 
 (* \section{Useful functions and flags} *)
@@ -172,7 +172,7 @@ let print_env_reification env =
   in
   let prop_info = str "ENVIRONMENT OF PROPOSITIONS :" ++ fnl () ++ loop 'P' 0 env.props in
   let term_info = str "ENVIRONMENT OF TERMS :" ++ fnl () ++ loop 'V' 0 env.terms in
-  msg_debug (prop_info ++ fnl () ++ term_info)
+  Feedback.msg_debug (prop_info ++ fnl () ++ term_info)
 
 (* \subsection{Gestion des environnements de variable pour Omega} *)
 (* generation d'identifiant d'equation pour Omega *)
@@ -454,7 +454,7 @@ let rec scalar n = function
  | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x))
  | Omult(t1,t2) ->
-     Errors.error "Omega: Can't solve a goal with non-linear products"
+     CErrors.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) -> do_list [], Omult(t,Oint n)
  | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i)
  | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n))
@@ -473,7 +473,7 @@ let rec negate = function
  | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x))
  | Omult(t1,t2) ->
-     Errors.error "Omega: Can't solve a goal with non-linear products"
+     CErrors.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) ->
      do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone))
  | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i)
@@ -545,7 +545,7 @@ let shrink_pair f1 f2 =
        Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2))
    | t1,t2 ->
        oprint stdout t1; print_newline (); oprint stdout t2; print_newline ();
-       flush Pervasives.stdout; Errors.error "shrink.1"
+       flush Pervasives.stdout; CErrors.error "shrink.1"
   end
 
 (* \subsection{Calcul d'une sous formule constante} *)
@@ -559,9 +559,9 @@ let reduce_factor = function
       let rec compute = function
           Oint n -> n
 	| Oplus(t1,t2) -> compute t1 + compute t2
-	| _ -> Errors.error "condense.1" in
+	| _ -> CErrors.error "condense.1" in
 	[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
-  | t -> Errors.error "reduce_factor.1"
+  | t -> CErrors.error "reduce_factor.1"
 
 (* \subsection{Réordonnancement} *)
 
@@ -1280,12 +1280,12 @@ let resolution env full_reified_goal systems_list =
     CCHyp{o_hyp=id_concl;o_path=[]} :: hyp_stated_vars @ initial_context in
   let decompose_tactic = decompose_tree env context solution_tree in
 
-  Tactics.generalize
-    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps)) >>
+  Proofview.V82.of_tactic (Tactics.generalize
+    (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >>
   Proofview.V82.of_tactic (Tactics.change_concl reified) >>
   Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
   show_goal >>
-  Tactics.normalise_vm_in_concl >>
+  Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >>
   (*i Alternatives to the previous line:
    - Normalisation without VM:
       Tactics.normalise_in_concl
@@ -1304,7 +1304,7 @@ let total_reflexive_omega_tactic gl =
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
   resolution env full_reified_goal systems_list gl
-  with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system"
+  with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
 
 
 (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
diff --git a/plugins/romega/romega_plugin.mllib b/plugins/romega/romega_plugin.mlpack
index 1625009d..38d0e941 100644
--- a/plugins/romega/romega_plugin.mllib
+++ b/plugins/romega/romega_plugin.mlpack
@@ -1,4 +1,3 @@
 Const_omega
 Refl_omega
 G_romega
-Romega_plugin_mod