Merge PR #1036: Unify EConstr.t equality

1 files changed, 6 insertions, 1 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7b879a8031..a54c082979 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