Merge PR #10714: Solve universe error with SSR 'rewrite !term'

Reviewed-by: ppedrot

4 files changed, 40 insertions, 22 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index ea71be8e43..c946125d3f 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -861,12 +861,12 @@ let compare_constructor_instances evd u u' =
   in
   Evd.add_universe_constraints evd soft
 
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
-    [u] up to existential variable instantiation and equalisable
-    universes. The term [t] is interpreted in [sigma1] while [u] is
-    interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extension of those in [sigma1]. *)
-let eq_constr_univs_test sigma1 sigma2 t u =
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+    [t] and [u] up to existential variable instantiation and
+    equalisable universes. The term [t] is interpreted in [evd] while
+    [u] is interpreted in [extended_evd]. The universe constraints in
+    [extended_evd] are assumed to be an extension of those in [evd]. *)
+let eq_constr_univs_test ~evd ~extended_evd t u =
   (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
   let open Evd in
   let t = EConstr.Unsafe.to_constr t
@@ -877,8 +877,8 @@ let eq_constr_univs_test sigma1 sigma2 t u =
   in
   let ans =
     UnivProblem.eq_constr_univs_infer_with
-      (fun t -> kind_of_term_upto sigma1 t)
-      (fun u -> kind_of_term_upto sigma2 u)
-      (universes sigma2) fold t u sigma2
+      (fun t -> kind_of_term_upto evd t)
+      (fun u -> kind_of_term_upto extended_evd u)
+      (universes extended_evd) fold t u extended_evd
   in
   match ans with None -> false | Some _ -> true
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index e9d579af32..7877b94582 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -204,12 +204,17 @@ val finalize : ?abort_on_undefined_evars:bool -> evar_map ->
 val kind_of_term_upto : evar_map -> Constr.constr ->
   (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) kind_of_term
 
-(** [eq_constr_univs_test sigma1 sigma2 t u] tests equality of [t] and
-    [u] up to existential variable instantiation and equalisable
-    universes. The term [t] is interpreted in [sigma1] while [u] is
-    interpreted in [sigma2]. The universe constraints in [sigma2] are
-    assumed to be an extension of those in [sigma1]. *)
-val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+(** [eq_constr_univs_test ~evd ~extended_evd t u] tests equality of
+    [t] and [u] up to existential variable instantiation and
+    equalisable universes. The term [t] is interpreted in [evd] while
+    [u] is interpreted in [extended_evd]. The universe constraints in
+    [extended_evd] are assumed to be an extension of those in [evd]. *)
+val eq_constr_univs_test :
+    evd:Evd.evar_map ->
+    extended_evd:Evd.evar_map ->
+    constr ->
+    constr ->
+    bool
 
 (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns
    [Inl sigma'] where [sigma'] is [sigma] augmented with universe
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8b8382ea53..1f076470c1 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -849,7 +849,8 @@ let give_up =
 
 module Progress = struct
 
-  let eq_constr = Evarutil.eq_constr_univs_test
+  let eq_constr evd extended_evd =
+    Evarutil.eq_constr_univs_test ~evd ~extended_evd
 
   (** equality function on hypothesis contexts *)
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
@@ -879,10 +880,10 @@ module Progress = struct
     eq_evar_body sigma1 sigma2 ei1.evar_body ei2.evar_body
 
   (** Equality function on goals *)
-  let goal_equal evars1 gl1 evars2 gl2 =
-    let evi1 = Evd.find evars1 gl1 in
-    let evi2 = Evd.find evars2 gl2 in
-    eq_evar_info evars1 evars2 evi1 evi2
+  let goal_equal ~evd ~extended_evd evar extended_evar =
+    let evi = Evd.find evd evar in
+    let extended_evi = Evd.find extended_evd extended_evar in
+    eq_evar_info evd extended_evd evi extended_evi
 
 end
 
@@ -899,7 +900,8 @@ let tclPROGRESS t =
   let test =
     quick_test ||
     Util.List.for_all2eq begin fun i f ->
-      Progress.goal_equal initial.solution (drop_state i) final.solution (drop_state f)
+      Progress.goal_equal ~evd:initial.solution
+        ~extended_evd:final.solution (drop_state i) (drop_state f)
     end initial.comb final.comb
   in
   if not test then
diff --git a/engine/proofview.mli b/engine/proofview.mli
index a17a1c9951..764a4a0058 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -398,7 +398,18 @@ val give_up : unit tactic
 val tclPROGRESS : 'a tactic -> 'a tactic
 
 module Progress : sig
-  val goal_equal : Evd.evar_map -> Evar.t -> Evd.evar_map -> Evar.t -> bool
+(** [goal_equal ~evd ~extended_evd evar extended_evar] tests whether
+    the [evar_info] from [evd] corresponding to [evar] is equal to that
+    from [extended_evd] corresponding to [extended_evar], up to
+    existential variable instantiation and equalisable universes. The
+    universe constraints in [extended_evd] are assumed to be an
+    extension of the universe constraints in [evd]. *)
+  val goal_equal :
+    evd:Evd.evar_map ->
+    extended_evd:Evd.evar_map ->
+    Evar.t ->
+    Evar.t ->
+    bool
 end
 
 (** Checks for interrupts *)