From d8176e6baaa33692ed82b9ac3c6e57e85f51dff0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Sat, 24 May 2014 15:13:47 +0200
Subject: Update infer_conv to record trivial Prop <= Type i constraints that
 are needed during unification.

---
 kernel/constr.ml | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index c6eacc289..fbcdc886b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -577,6 +577,52 @@ let leq_constr_univs univs m n =
     and leq_constr' m n = m == n || compare_leq m n in
       compare_leq m n
 
+let eq_constr_univs_infer univs m n =
+  if m == n then true, Constraint.empty
+  else 
+    let cstrs = ref Constraint.empty in
+    let eq_universes strict = Univ.Instance.check_eq univs 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
+	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+	   true)
+    in
+    let rec eq_constr' m n = 
+      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
+    in
+    let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
+      res, !cstrs
+
+let leq_constr_univs_infer univs m n =
+  if m == n then true, Constraint.empty
+  else 
+    let cstrs = ref Constraint.empty in
+    let eq_universes strict l l' = Univ.Instance.check_eq 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
+	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+	   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
+	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
+	   true)
+    in
+    let rec eq_constr' m n = 
+      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
+    in
+    let rec compare_leq m n =
+      compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+    and leq_constr' m n = m == n || compare_leq m n in
+    let res = compare_leq m n in
+      res, !cstrs
+
 let eq_constr_universes m n =
   if m == n then true, UniverseConstraints.empty
   else 
-- 
cgit v1.2.3