From 744e49018cb5c9cfb662c950433c82006ca64988 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 28 May 2014 16:06:22 +0200
Subject: - 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).

---
 kernel/reduction.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'kernel/reduction.ml')

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