Tactical `progress` compares term up to potentially equalisable universes.

Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.

As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.

4 files changed, 27 insertions, 8 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 201a16ebeb..2508f4ef3b 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -844,6 +844,25 @@ let subterm_source evk (loc,k) =
   (loc,Evar_kinds.SubEvar evk)
 
 
-(** Term exploration up to isntantiation. *)
+(** Term exploration up to instantiation. *)
 let kind_of_term_upto sigma t =
   Constr.kind (Reductionops.whd_evar sigma t)
+
+(** [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 extention of those in [sigma1]. *)
+let eq_constr_univs_test sigma1 sigma2 t u =
+  (* spiwack: mild code duplication with {!Evd.eq_constr_univs}. *)
+  let open Evd in
+  let b, c =
+    Universes.eq_constr_univs_infer_with
+      (fun t -> kind_of_term_upto sigma1 t)
+      (fun u -> kind_of_term_upto sigma2 u)
+      (universes sigma2) t u
+  in
+  if b then
+    try let _ = add_universe_constraints sigma2 c in true
+    with Univ.UniverseInconsistency _ | UniversesDiffer -> false
+  else false
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 49036798e6..f1d94b0a4f 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -206,6 +206,13 @@ val flush_and_check_evars :  evar_map -> constr -> constr
     value of [e] in [sigma] is (recursively) used. *)
 val kind_of_term_upto : evar_map -> constr -> (constr,types) 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 extention of those in [sigma1]. *)
+val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
+
 (** {6 debug pretty-printer:} *)
 
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index bf519fb7c0..f414d71dc1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1304,9 +1304,6 @@ let e_eq_constr_univs evdref t u =
   let evd, b = eq_constr_univs !evdref t u in
     evdref := evd; b
 
-let eq_constr_univs_test evd t u =
-  snd (eq_constr_univs evd t u)
-
 (**********************************************************)
 (* Accessing metas *)
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fe785a8314..eca6d60ad5 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -562,10 +562,6 @@ val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
 val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
 (** Syntactic equality up to universes. *)
 
-val eq_constr_univs_test : evar_map -> constr -> constr -> bool
-(** Syntactic equality up to universes, throwing away the (consistent) constraints
-    in case of success. *)
-
 (********************************************************************)
 (* constr with holes and pending resolution of classes, conversion  *)
 (* problems, candidates, etc.                                       *)