Using EConstr equality check in unification.

The code from Universes what essentially a duplicate of the one from EConstr,
but they were copied for historical reasons. Now, this is not useful anymore,
so that we remove the implementation from Universes and rely on the one from
EConstr.

4 files changed, 4 insertions, 103 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7b879a8031..66b50fc25e 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -566,7 +566,6 @@ let compare_constr sigma cmp c1 c2 =
   let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in
   compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2)
 
-(** TODO: factorize with universes.ml *)
 let test_constr_universes sigma leq m n =
   let open Universes in
   let kind c = kind_upto sigma c in
diff --git a/engine/universes.ml b/engine/universes.ml
index 719af43edf..686411e7d5 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -131,47 +131,6 @@ let to_constraints g s =
 		   "to_constraints: non-trivial algebraic constraint between universes")
   in Constraints.fold tr s Constraint.empty
 
-let test_constr_univs_infer leq univs fold m n accu =
-  if m == n then Some accu
-  else 
-    let cstrs = ref accu in
-    let eq_universes strict l l' = UGraph.check_eq_instances univs l l' 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
-	match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
-	| None -> false
-	| Some accu -> cstrs := accu; 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
-	match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with
-	| None -> false
-	| Some accu -> cstrs := accu; true
-    in
-    let rec eq_constr' m n = 
-      m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
-    in
-    let res =
-      if leq then
-        let rec compare_leq 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
-        compare_leq m n
-      else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
-    in
-    if res then Some !cstrs else None
-
-let eq_constr_univs_infer univs fold m n accu =
-  test_constr_univs_infer false univs fold m n accu
-
-let leq_constr_univs_infer univs fold m n accu =
-  test_constr_univs_infer true univs fold m n accu
-
 (** 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 fold m n accu =
@@ -197,42 +156,6 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
   let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
   if res then Some !cstrs else None
 
-let test_constr_universes leq m n =
-  if m == n then Some Constraints.empty
-  else 
-    let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = 
-      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
-      if Sorts.equal s1 s2 then true
-      else (cstrs := Constraints.add 
-	      (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; 
-	    true)
-    in
-    let leq_sorts s1 s2 = 
-      if Sorts.equal s1 s2 then true
-      else 
-	(cstrs := Constraints.add 
-	   (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; 
-	 true)
-    in
-    let rec eq_constr' m n = 
-      m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
-    in
-    let res =
-      if leq then
-        let rec compare_leq 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
-        compare_leq m n
-      else
-        Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
-    in
-    if res then Some !cstrs else None
-
-let eq_constr_universes m n = test_constr_universes false m n
-let leq_constr_universes m n = test_constr_universes true m n
-
 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)
diff --git a/engine/universes.mli b/engine/universes.mli
index fe40f82385..8b2217d446 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -67,11 +67,6 @@ val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_f
 
 val to_constraints : UGraph.t -> universe_constraints -> constraints
 
-(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts,
-   application grouping, the universe constraints in [u] and additional constraints [c]. *)
-val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
-  constr -> constr -> 'a -> 'a option
-
 (** [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. *)
@@ -80,20 +75,6 @@ val eq_constr_univs_infer_with :
   (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) ->
   UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option
 
-(** [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]. *)
-val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator ->
-  constr -> constr -> 'a -> 'a option
-
-(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
-    application grouping and the universe constraints in [c]. *)
-val eq_constr_universes : constr -> constr -> universe_constraints option
-
-(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
-    alpha, casts, application grouping and the universe constraints in [c]. *)
-val leq_constr_universes : constr -> constr -> universe_constraints option
-
 (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
     application grouping and the universe constraints in [c]. *)
 val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3563235434..2aa2f90131 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1438,17 +1438,13 @@ let sigma_univ_state =
 let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
   (** FIXME *)
-  let open Universes in
-  let x = EConstr.Unsafe.to_constr x in
-  let y = EConstr.Unsafe.to_constr y in
   try
-    let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in
     let b, sigma = 
       let ans =
 	if pb == Reduction.CUMUL then 
-	  Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
+	  EConstr.leq_constr_universes sigma x y
 	else
-	  Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty
+	  EConstr.eq_constr_universes sigma x y
       in
       let ans = match ans with
       | None -> None
@@ -1462,6 +1458,8 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     in
       if b then sigma, true
       else
+        let x = EConstr.Unsafe.to_constr x in
+        let y = EConstr.Unsafe.to_constr y in
 	let sigma' = 
 	  conv_fun pb ~l2r:false sigma ts
 	    env (sigma, sigma_univ_state) x y in