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.

2 files changed, 54 insertions, 20 deletions

diff --git a/library/universes.ml b/library/universes.ml
index 9fddc7067b..3a8ee26254 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -139,6 +139,32 @@ let eq_constr_univs_infer univs m n =
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
       res, !cstrs
 
+(** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
+    to expose subterms of [m] and [n], arguments. *)
+let eq_constr_univs_infer_with kind1 kind2 univs m n =
+  (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
+     haven't find a way to factor the code without destroying
+     pointer-equality optimisations in [eq_constr_univs_infer].
+     Pointer equality is not sufficient to ensure equality up to
+     [kind1,kind2], because [kind1] and [kind2] may be different,
+     typically evaluating [m] and [n] in different evar maps. *)
+  let cstrs = ref Constraints.empty in
+  let eq_universes strict = Univ.Instance.check_eq univs in
+  let eq_sorts s1 s2 = 
+    if Sorts.equal s1 s2 then true
+    else
+      let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
+      if Univ.check_eq univs u1 u2 then true
+      else
+	(cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+	 true)
+  in
+  let rec eq_constr' m n = 
+    Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
+  in
+  let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
+  res, !cstrs
+
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraints.empty
   else 
@@ -148,18 +174,18 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-		true)
+	if Univ.check_eq univs u1 u2 then true
+	else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
+	      true)
     in
     let leq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then true
-	  else
-	    (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
-	     true)
+	if Univ.check_leq univs u1 u2 then true
+	else
+	  (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -169,7 +195,7 @@ let leq_constr_univs_infer univs m n =
 	eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-      res, !cstrs
+    res, !cstrs
 
 let eq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -188,7 +214,7 @@ let eq_constr_universes m n =
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 let leq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -216,22 +242,22 @@ let leq_constr_universes m n =
       Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-      res, !cstrs
+    res, !cstrs
 
 let compare_head_gen_proj env equ eqs eqc' m n =
   match kind_of_term m, kind_of_term n with
   | Proj (p, c), App (f, args)
   | App (f, args), Proj (p, c) -> 
-    (match kind_of_term f with
-    | Const (p', u) when eq_constant (Projection.constant p) p' -> 
-      let pb = Environ.lookup_projection p env in
-      let npars = pb.Declarations.proj_npars in
-	if Array.length args == npars + 1 then
-	  eqc' c args.(npars)
-	else false
-    | _ -> false)
+      (match kind_of_term f with
+      | Const (p', u) when eq_constant (Projection.constant p) p' -> 
+          let pb = Environ.lookup_projection p env in
+          let npars = pb.Declarations.proj_npars in
+	  if Array.length args == npars + 1 then
+	    eqc' c args.(npars)
+	  else false
+      | _ -> false)
   | _ -> Constr.compare_head_gen equ eqs eqc' m n
-    
+      
 let eq_constr_universes_proj env m n =
   if m == n then true, Constraints.empty
   else 
@@ -249,7 +275,7 @@ let eq_constr_universes_proj env m n =
       m == n ||	compare_head_gen_proj env eq_universes eq_sorts eq_constr' m n
     in
     let res = eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 (* Generator of levels *)
 let new_univ_level, set_remote_new_univ_level =
diff --git a/library/universes.mli b/library/universes.mli
index 252648d7dc..5527da0903 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -66,6 +66,14 @@ val to_constraints : universes -> universe_constraints -> constraints
    application grouping, the universe constraints in [u] and additional constraints [c]. *)
 val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
 
+(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
+    {!eq_constr_univs_infer} taking kind-of-term functions, to expose
+    subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  Univ.universes -> constr -> constr -> bool universe_constrained
+
 (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
     modulo alpha, casts, application grouping, the universe constraints
     in [u] and additional constraints [c]. *)