- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some

cases of Type (* Prop *) <= Set.
- Do check types of metavariables at the end of apply's unification,
if it failed at the beginning (otherwise universe constraints can be incomplete).

2 files changed, 12 insertions, 19 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a820e337ef..5024675bff 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -167,12 +167,6 @@ let convert_universes (univs,cstrs as cuniv) u u' =
     | None -> raise NotConvertible
     | Some cstrs -> 
       (univs, Some (Univ.enforce_eq_instances u u' cstrs)))
-
-      (* try  *)
-      (* 	let cstr = Univ.enforce_eq_instances u u' Univ.Constraint.empty in *)
-      (* 	let univs' = Univ.enforce_constraint cstr univs in *)
-      (* 	  (univs', Some (Univ.enforce_eq_instances u u' cstrs)) *)
-      (* with UniverseInconsistency _ -> raise NotConvertible) *)
       
 let conv_table_key k1 k2 cuniv =
   match k1, k2 with
@@ -632,8 +626,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
     if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 
     else Constr.eq_constr_univs_infer univs t1 t2
   in
-    if b && (try ignore(Univ.merge_constraints cstrs univs); true with _ -> false) then 
-      cstrs
+    if b then cstrs
     else 
       let (u, cstrs) = 
 	clos_fconv reds cv_pb l2r evars env (univs, Some Constraint.empty) t1 t2 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7ab0aa93c1..8984938d36 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1198,9 +1198,9 @@ let fast_compare g arcu arcv =
 
 let is_leq g arcu arcv =
   arcu == arcv ||
- (match fast_compare_neq false g arcu arcv with
- | FastNLE -> false
- | (FastEQ|FastLE|FastLT) -> true)
+    (match fast_compare_neq false g arcu arcv with
+    | FastNLE -> false
+    | (FastEQ|FastLE|FastLT) -> true)
     
 let is_lt g arcu arcv =
   if arcu == arcv then false
@@ -1241,7 +1241,7 @@ let check_smaller g strict u v =
     let proparc = prop_arc g in
       arcu == proparc ||
 	((arcv != proparc && arcu == set_arc g) ||
-	     is_leq g arcu arcv)
+	    is_leq g arcu arcv)
 
 (** Then, checks on universes *)
 
@@ -1345,17 +1345,17 @@ let merge g arcu arcv =
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
-    match between g arcu arcv with
+      match between g arcu arcv with
       | [] -> anomaly (str "Univ.between")
       | arc::rest ->
         let (max_rank, old_max_rank, best_arc, rest) =
           List.fold_left best_ranked (arc.rank, min_int, arc, []) rest in
-        if max_rank > old_max_rank then best_arc, g, rest
-        else begin
-          (* one redirected node also has max_rank *)
-          let arcu = {best_arc with rank = max_rank + 1} in
-          arcu, enter_arc arcu g, rest
-        end 
+          if max_rank > old_max_rank then best_arc, g, rest
+          else begin
+              (* one redirected node also has max_rank *)
+            let arcu = {best_arc with rank = max_rank + 1} in
+	      arcu, enter_arc arcu g, rest
+          end 
   in
   let redirect (g,w,w') arcv =
     let g' = enter_equiv_arc arcv.univ arcu.univ g in