Rename eq_constr functions in Evd to not break backward compatibility

with existing ML code.

6 files changed, 18 insertions, 16 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3b3c9f9ee..eba0423fe 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -840,7 +840,7 @@ let apply_on_subterm env evdref f c t =
     (* By using eq_constr, we make an approximation, for instance, we *)
     (* could also be interested in finding a term u convertible to t *)
     (* such that c occurs in u *)
-    if e_eq_constr evdref c t then f k
+    if e_eq_constr_univs evdref c t then f k
     else
       match kind_of_term t with
       | Evar (evk,args) when Evd.is_undefined !evdref evk ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ba877d35c..a41e0169a 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1173,7 +1173,7 @@ type conv_fun_bool =
 
 let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 =
   let evdref = ref evd in
-  if Array.equal (e_eq_constr evdref) argsv1 argsv2 then !evdref else
+  if Array.equal (e_eq_constr_univs evdref) argsv1 argsv2 then !evdref else
   (* Filter and restrict if needed *)
   let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in
   let untypedfilter =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e49ed7b45..63e25a541 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1333,35 +1333,36 @@ let test_conversion env d pb t u =
   try conversion_gen env d pb t u; true
   with _ -> false
 
-let eq_constr evd t u =
+let eq_constr_univs evd t u =
   let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
     if b then 
       try let evd' = add_universe_constraints evd c in evd', b
       with Univ.UniverseInconsistency _ -> evd, false
     else evd, b
 
-let e_eq_constr evdref t u =
-  let evd, b = eq_constr !evdref t u in
+let e_eq_constr_univs evdref t u =
+  let evd, b = eq_constr_univs !evdref t u in
     evdref := evd; b
 
-let eq_constr_test evd t u =
-  snd (eq_constr evd t u)
+let eq_constr_univs_test evd t u =
+  snd (eq_constr_univs evd t u)
 
 let eq_named_context_val d ctx1 ctx2 = 
   ctx1 == ctx2 ||
     let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in
     let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-      Id.equal i1 i2 && Option.equal (eq_constr_test d) c1 c2 && (eq_constr_test d) t1 t2
+      Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 
+      && (eq_constr_univs_test d) t1 t2
     in List.equal eq_named_declaration c1 c2
 
 let eq_evar_body d b1 b2 = match b1, b2 with
 | Evar_empty, Evar_empty -> true
-| Evar_defined t1, Evar_defined t2 -> eq_constr_test d t1 t2
+| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2
 | _ -> false
 
 let eq_evar_info d ei1 ei2 =
   ei1 == ei2 ||
-    eq_constr_test d ei1.evar_concl ei2.evar_concl &&
+    eq_constr_univs_test d ei1.evar_concl ei2.evar_concl &&
     eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) &&
     eq_evar_body d ei1.evar_body ei2.evar_body
     (** ppedrot: [eq_constr] may be a bit too permissive here *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index b284bd42c..db4515ae8 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -518,13 +518,13 @@ val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map
 val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool
 (** This one forgets about the assignemts of universes. *)
 
-val eq_constr : evar_map -> constr -> constr -> evar_map * bool
+val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool
 (** Syntactic equality up to universes, recording the associated constraints *)
 
-val e_eq_constr : evar_map ref -> constr -> constr -> bool
+val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool
 (** Syntactic equality up to universes. *)
 
-val eq_constr_test : evar_map -> constr -> constr -> bool
+val eq_constr_univs_test : evar_map -> constr -> constr -> bool
 (** Syntactic equality up to universes, throwing away the (consistent) constraints
     in case of success. *)
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 51ca5ddda..0647fa813 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -780,7 +780,7 @@ END
 let eq_constr x y = 
   Proofview.Goal.enter (fun gl ->
     let evd = Proofview.Goal.sigma gl in
-      if Evd.eq_constr_test evd x y then Proofview.tclUNIT () 
+      if Evd.eq_constr_univs_test evd x y then Proofview.tclUNIT () 
       else Tacticals.New.tclFAIL 0 (str "Not equal"))
 
 TACTIC EXTEND constr_eq
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 841116a0b..f14810482 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4033,8 +4033,9 @@ let intros_transitivity  n  = Tacticals.New.tclTHEN intros (transitivity_gen n)
 (** d1 is the section variable in the global context, d2 in the goal context *)
 let interpretable_as_section_decl evd d1 d2 = match d2,d1 with
   | (_,Some _,_), (_,None,_) -> false
-  | (_,Some b1,t1), (_,Some b2,t2) -> e_eq_constr evd b1 b2 && e_eq_constr evd t1 t2
-  | (_,None,t1), (_,_,t2) -> e_eq_constr evd t1 t2
+  | (_,Some b1,t1), (_,Some b2,t2) -> 
+    e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2
+  | (_,None,t1), (_,_,t2) -> e_eq_constr_univs evd t1 t2
 
 let abstract_subproof id gk tac =
   let open Tacticals.New in