Imported Upstream version 8.9.0upstream/8.9.0upstream

4 files changed, 23 insertions, 19 deletions

diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 59fd9b80..94a3d404 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -85,6 +85,7 @@ Ltac zify_binop t thm a b:=
 
 Ltac zify_op_1 :=
   match goal with
+   | x := ?t : Z |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
    | |- context [ Z.max ?a ?b ] => zify_binop Z.max Z.max_spec a b
    | H : context [ Z.max ?a ?b ] |- _ => zify_binop Z.max Z.max_spec a b
    | |- context [ Z.min ?a ?b ] => zify_binop Z.min Z.min_spec a b
@@ -114,6 +115,7 @@ Ltac hide_Z_of_nat t :=
 Ltac zify_nat_rel :=
  match goal with
   (* I: equalities *)
+  | x := ?t : nat |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
   | |- (@eq nat ?a ?b) => apply (Nat2Z.inj a b) (* shortcut *)
   | H : context [ @eq nat ?a ?b ] |- _ => rewrite <- (Nat2Z.inj_iff a b) in H
   | |- context [ @eq nat ?a ?b ] =>       rewrite <- (Nat2Z.inj_iff a b)
@@ -181,7 +183,7 @@ Ltac zify_nat_op :=
         let t := eval compute in (Z.of_nat (S a)) in
         change (Z.of_nat (S a)) with t in H
       | _ => rewrite (Nat2Z.inj_succ a) in H
-      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+      | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
                 hide [Z.of_nat (S a)] in this one hypothesis *)
         change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H
      end
@@ -192,7 +194,7 @@ Ltac zify_nat_op :=
         let t := eval compute in (Z.of_nat (S a)) in
         change (Z.of_nat (S a)) with t
       | _ => rewrite (Nat2Z.inj_succ a)
-      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+      | _ => (* if the [rewrite] fails (most likely a dependent occurrence of [Z.of_nat (S a)]),
                 hide [Z.of_nat (S a)] in the goal *)
         change (Z.of_nat (S a)) with (Z_of_nat' (S a))
      end
@@ -223,6 +225,7 @@ Ltac hide_Zpos t :=
 Ltac zify_positive_rel :=
  match goal with
   (* I: equalities *)
+  | x := ?t : positive |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
   | |- (@eq positive ?a ?b) => apply Pos2Z.inj
   | H : context [ @eq positive ?a ?b ] |- _ => rewrite <- (Pos2Z.inj_iff a b) in H
   | |- context [ @eq positive ?a ?b ] =>       rewrite <- (Pos2Z.inj_iff a b)
@@ -348,6 +351,7 @@ Ltac hide_Z_of_N t :=
 Ltac zify_N_rel :=
  match goal with
   (* I: equalities *)
+  | x := ?t : N |- _ => let h := fresh "heq_" x in pose proof (eq_refl : x = t) as h; clearbody x
   | |- (@eq N ?a ?b) => apply (N2Z.inj a b) (* shortcut *)
   | H : context [ @eq N ?a ?b ] |- _ => rewrite <- (N2Z.inj_iff a b) in H
   | |- context [ @eq N ?a ?b ] =>       rewrite <- (N2Z.inj_iff a b)
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 51cd665f..e14c4e2e 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -18,8 +18,8 @@
 open CErrors
 open Util
 open Names
+open Constr
 open Nameops
-open Term
 open EConstr
 open Tacticals.New
 open Tacmach.New
@@ -29,7 +29,7 @@ open Libnames
 open Globnames
 open Nametab
 open Contradiction
-open Misctypes
+open Tactypes
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -38,15 +38,9 @@ open OmegaSolver
 
 (* Added by JCF, 09/03/98 *)
 
-let elim_id id =
-  Proofview.Goal.enter begin fun gl ->
-    simplest_elim (mkVar id)
-  end
-let resolve_id id = Proofview.Goal.enter begin fun gl ->
-  apply (mkVar id)
-end
+let elim_id id = simplest_elim (mkVar id)
 
-let timing timer_name f arg = f arg
+let resolve_id id = apply (mkVar id)
 
 let display_time_flag = ref false
 let display_system_flag = ref false
@@ -206,7 +200,7 @@ let coq_modules =
   init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
     @ [["Coq"; "omega"; "OmegaLemmas"]]
 
-let gen_constant_in_modules n m s = EConstr.of_constr (Universes.constr_of_global @@ gen_reference_in_modules n m s)
+let gen_constant_in_modules n m s = EConstr.of_constr (UnivGen.constr_of_global @@ gen_reference_in_modules n m s)
 let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
@@ -369,8 +363,11 @@ let coq_True = lazy (init_constant "True")
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
 (* For unfold *)
-let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with
-  | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+let evaluable_ref_of_constr s c =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  match EConstr.kind evd (Lazy.force c) with
+  | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) ->
       EvalConstRef kn
   | _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
 
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.mlg
index 170b937c..c3d063cf 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.mlg
@@ -18,6 +18,8 @@
 
 DECLARE PLUGIN "omega_plugin"
 
+{
+
 open Ltac_plugin
 open Names
 open Coq_omega
@@ -43,14 +45,15 @@ let omega_tactic l =
     (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs))
     (omega_solver)
 
+}
 
 TACTIC EXTEND omega
-|  [ "omega" ] -> [ omega_tactic [] ]
+|  [ "omega" ] -> { omega_tactic [] }
 END
 
 TACTIC EXTEND omega'
 | [ "omega" "with" ne_ident_list(l) ] ->
-    [ omega_tactic (List.map Names.Id.to_string l) ]
-| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ]
+    { omega_tactic (List.map Names.Id.to_string l) }
+| [ "omega" "with" "*" ] -> { omega_tactic ["nat";"positive";"N";"Z"] }
 END
 
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 2510c169..7bca7c70 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.ml
@@ -178,7 +178,7 @@ let rec display_action print_var = function
       | DIVIDE_AND_APPROX (e1,e2,k,d) ->
           Printf.printf
             "Inequation E%d is divided by %s and the constant coefficient is \
-            rounded by substracting %s.\n" e1.id (sbi k) (sbi d)
+            rounded by subtracting %s.\n" e1.id (sbi k) (sbi d)
       | NOT_EXACT_DIVIDE (e,k) ->
           Printf.printf
             "Constant in equation E%d is not divisible by the pgcd \