Solve universe error with SSR 'rewrite !term'

1 files changed, 11 insertions, 6 deletions

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