1 files changed, 16 insertions, 7 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 418229330..9bf743152 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -130,8 +130,8 @@ let mkProp   = Sort Sorts.prop
 let mkSet    = Sort Sorts.set
 let mkType u = Sort (Sorts.Type u)
 let mkSort   = function
-  | Sorts.Prop Sorts.Null -> mkProp (* Easy sharing *)
-  | Sorts.Prop Sorts.Pos -> mkSet
+  | Sorts.Prop -> mkProp (* Easy sharing *)
+  | Sorts.Set -> mkSet
   | s -> Sort s
 
 (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *)
@@ -260,17 +260,17 @@ let isSort c = match kind c with
   | _ -> false
 
 let rec isprop c = match kind c with
-  | Sort (Sorts.Prop _) -> true
+  | Sort (Sorts.Prop | Sorts.Set) -> true
   | Cast (c,_,_) -> isprop c
   | _ -> false
 
 let rec is_Prop c = match kind c with
-  | Sort (Sorts.Prop Sorts.Null) -> true
+  | Sort Sorts.Prop -> true
   | Cast (c,_,_) -> is_Prop c
   | _ -> false
 
 let rec is_Set c = match kind c with
-  | Sort (Sorts.Prop Sorts.Pos) -> true
+  | Sort Sorts.Set -> true
   | Cast (c,_,_) -> is_Set c
   | _ -> false
 
@@ -828,8 +828,10 @@ let leq_constr_univs_infer univs m n =
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
 	if UGraph.check_leq univs u1 u2 then true
 	else
-	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
-	   true)
+          (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in
+            cstrs := Univ.Constraint.union c !cstrs;
+            true
+          with Univ.UniverseInconsistency _ -> false)
     in
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
@@ -1207,3 +1209,10 @@ let hcons =
      Id.hcons)
 
 (* let hcons_types = hcons_constr *)
+
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt
+type rel_context = rel_declaration list
+type named_context = named_declaration list
+type compacted_context = compacted_declaration list