- 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.

1 files changed, 2 insertions, 0 deletions

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"
     
 (********************************************************************)