From 105db906ae45e792d1caeeb2e3fb7f69944b2caa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 12:53:41 +0200
Subject: - Fixes for canonical structure resolution (check that the initial
 term indeed unifies with the projected term, keeping track of universes). -
 Fix the [unify] tactic to fail properly. - Fix unification to disallow
 lowering a global Type(i) universe to Prop or Set.

---
 pretyping/reductionops.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b64156649f..7022946e57 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1024,6 +1024,7 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
     | Reduction.CUMUL -> Reduction.trans_conv_leq_universes in
     try f ~evars:(safe_evar_value sigma) ts env (Evd.universes sigma) x y; true
     with Reduction.NotConvertible -> false
+    | Univ.UniverseInconsistency _ -> false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
 let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = 
@@ -1034,6 +1035,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
       let cstrs = f ~evars:(safe_evar_value sigma) ~ts env (Evd.universes sigma) x y in
 	Evd.add_constraints sigma cstrs, true
     with Reduction.NotConvertible -> sigma, false
+    | Univ.UniverseInconsistency _ -> sigma, false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
     
 (********************************************************************)
-- 
cgit v1.2.3