Solve universe error with SSR 'rewrite !term'

7 files changed, 58 insertions, 24 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 8b5bd4cd80..1fbad25d46 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 f90f02f3e1..d6ca94e405 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 *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 888c4785df..f95a904a5f 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -91,7 +91,8 @@ module V82 = struct
 
   let weak_progress glss gls =
     match glss.Evd.it with
-    | [ g ] -> not (Proofview.Progress.goal_equal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
+    | [ g ] -> not (Proofview.Progress.goal_equal ~evd:gls.Evd.sigma
+                      ~extended_evd:glss.Evd.sigma gls.Evd.it g)
     | _ -> true
 
   let progress glss gls =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 220b9bc475..1f125a3c59 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -255,7 +255,9 @@ let tclNOTSAMEGOAL tac =
     Proofview.Goal.goals >>= fun gls ->
     let check accu gl' =
       gl' >>= fun gl' ->
-      let accu = accu || Proofview.Progress.goal_equal sigma ev (project gl') (goal gl') in
+      let accu = accu || Proofview.Progress.goal_equal
+                            ~evd:sigma ~extended_evd:(project gl') ev (goal gl')
+      in
       Proofview.tclUNIT accu
     in
     Proofview.Monad.List.fold_left check false gls >>= fun has_same ->
diff --git a/test-suite/ssr/bang_rewrite.v b/test-suite/ssr/bang_rewrite.v
new file mode 100644
index 0000000000..30e6d57a7a
--- /dev/null
+++ b/test-suite/ssr/bang_rewrite.v
@@ -0,0 +1,13 @@
+Set Universe Polymorphism.
+
+Require Import ssreflect.
+
+Axiom mult@{i} : nat -> nat -> nat.
+Notation "m * n" := (mult m n).
+
+Axiom multA : forall a b c, (a * b) * c = a * (b * c).
+
+(* Previously the following gave a universe error: *)
+
+Lemma multAA a b c d : ((a * b) * c) * d = a * (b * (c * d)).
+Proof. by rewrite !multA. Qed.