From a9f8fa56e76aa557b1391cb9709cb893a4f602ce Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Aug 2017 12:37:36 +0200
Subject: 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.
---
 engine/eConstr.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'engine/eConstr.ml')

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
-- 
cgit v1.2.3


From 7760c6d58ca35b97b0893dc4911ab22c9a5a49ec Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Aug 2017 13:06:48 +0200
Subject: Normalizing universes before performing term comparison.

This code was probably slightly wrong w.r.t. to a semantics defined as
equivalent to first full-blown normalization followed by kernel term equality.
Or at least, it was adding redundant constraints.
---
 engine/eConstr.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 66b50fc25e..a54c082979 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -573,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 
-- 
cgit v1.2.3