Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

3 files changed, 23 insertions, 14 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index b84cf25405..36511386ac 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1492,7 +1492,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/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 0a99a26b36..61efa9f545 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,15 +10,24 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Names
 open Refl_omega
+open Constrarg
+open Pcoq.Prim
+
+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>>
+       | "nat" -> eval_tactic "zify_nat"
+       | "positive" -> eval_tactic "zify_positive"
+       | "N" -> eval_tactic "zify_N"
+       | "Z" -> eval_tactic "zify_op"
        | s -> Errors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 8156e84114..177c870b3c 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -44,9 +44,9 @@ let occ_step_eq s1 s2 = match s1, s2 with
 
 (* chemin identifiant une proposition sous forme du nom de l'hypothèse et
    d'une liste de pas à partir de la racine de l'hypothèse *)
-type occurence = {o_hyp : Names.Id.t; o_path : occ_path}
+type occurrence = {o_hyp : Names.Id.t; o_path : occ_path}
 
-(* \subsection{refiable formulas} *)
+(* \subsection{reifiable formulas} *)
 type oformula =
     (* integer *)
   | Oint of Bigint.bigint
@@ -55,7 +55,7 @@ type oformula =
   | Omult of oformula * oformula
   | Ominus of oformula * oformula
   | Oopp of  oformula
-    (* an atome in the environment *)
+    (* an atom in the environment *)
   | Oatom of int
     (* weird expression that cannot be translated *)
   | Oufo of oformula
@@ -75,13 +75,13 @@ type oproposition =
   | Pimp of int * oproposition * oproposition
   | Pprop of Term.constr
 
-(* Les équations ou proposiitions atomiques utiles du calcul *)
+(* Les équations ou propositions atomiques utiles du calcul *)
 and oequation = {
     e_comp: comparaison;		(* comparaison *)
     e_left: oformula;			(* formule brute gauche *)
     e_right: oformula;			(* formule brute droite *)
     e_trace: Term.constr;		(* tactique de normalisation *)
-    e_origin: occurence;		(* l'hypothèse dont vient le terme *)
+    e_origin: occurrence;		(* l'hypothèse dont vient le terme *)
     e_negated: bool;			(* vrai si apparait en position nié
 					   après normalisation *)
     e_depends: direction  list;		(* liste des points de disjonction dont
@@ -111,7 +111,7 @@ type environment = {
   real_indices : (int,int) Hashtbl.t;
   mutable cnt_connectors : int;
   equations : (int,oequation) Hashtbl.t;
-  constructors : (int, occurence) Hashtbl.t
+  constructors : (int, occurrence) Hashtbl.t
 }
 
 (* \subsection{Solution tree}
@@ -136,7 +136,7 @@ type solution_tree =
    chemins pour extraire des equations ou d'hypothèses *)
 
 type context_content =
-    CCHyp of occurence
+    CCHyp of occurrence
   | CCEqua of int
 
 (* \section{Specific utility functions to handle base types} *)
@@ -1266,7 +1266,7 @@ let resolution env full_reified_goal systems_list =
       |	(O_right :: l) -> app coq_p_right [| loop l |] in
     let correct_index =
       let i = List.index0 Names.Id.equal e.e_origin.o_hyp l_hyps in
-      (* PL: it seems that additionnally introduced hyps are in the way during
+      (* PL: it seems that additionally introduced hyps are in the way during
              normalization, hence this index shifting... *)
       if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce)
     in
@@ -1285,7 +1285,7 @@ let resolution env full_reified_goal systems_list =
   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