From 15999903f875f4b5dbb3d5240d2ca39acc3cd777 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 26 May 2014 13:58:56 +0200
Subject: - Fix in kernel conversion not folding the universe constraints
 correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints,
 that would otherwise allow constraints that make a universe lower than Prop.
 - Fix stm/lemmas that was pushing constraints to the global context, it is
 done depending on the constant/variable polymorphic status now. - Adapt
 generalized rewriting in Type code to these fixes.

---
 pretyping/evd.ml         | 2 ++
 pretyping/unification.ml | 4 ++--
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1f462197c8..940a54128c 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1132,6 +1132,8 @@ let set_leq_sort evd s1 s2 =
       | Prop c, Prop c' -> 
 	  if c == Null && c' == Pos then evd
 	  else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])))
+      | Type _, Prop _ ->
+	raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))
       | _, _ -> 
         add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2))
 	    
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7b6fb262a8..1b2afd19a5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -33,7 +33,6 @@ let occur_meta_or_undefined_evar evd c =
         | Evar_defined c ->
             occrec c; Array.iter occrec args
         | Evar_empty -> raise Occur)
-    (* | Sort (Type _) (\* FIXME could be finer *\) -> raise Occur *)
     | Const (_, i) (* | Ind (_, i) | Construct (_, i)  *)
 	when not (Univ.Instance.is_empty i) -> raise Occur
     | _ -> iter_constr occrec c
@@ -749,7 +748,8 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       with Invalid_argument "Reductionops.Stack.fold2" ->
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
     else error_cannot_unify (fst curenvnb) sigma (cM,cN)
-      in
+  in
+    
   let res = 
     if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n
       || subterm_restriction conv_at_top flags then None
-- 
cgit v1.2.3