Merge PR #1036: Unify EConstr.t equality

3 files changed, 6 insertions, 97 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7b879a803..a54c08297 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
@@ -574,14 +573,20 @@ let test_constr_universes sigma leq m n =
   else 
     let cstrs = ref Constraints.empty in
     let eq_universes strict l l' = 
+      let l = EInstance.kind sigma (EInstance.make l) in
+      let l' = EInstance.kind sigma (EInstance.make l') in
       cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
     let eq_sorts s1 s2 = 
+      let s1 = ESorts.kind sigma (ESorts.make s1) in
+      let s2 = ESorts.kind sigma (ESorts.make s2) in
       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 = 
+      let s1 = ESorts.kind sigma (ESorts.make s1) in
+      let s2 = ESorts.kind sigma (ESorts.make s2) in
       if Sorts.equal s1 s2 then true
       else 
 	(cstrs := Constraints.add 
diff --git a/engine/universes.ml b/engine/universes.ml
index 719af43ed..686411e7d 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 fe40f8238..8b2217d44 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