diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-26 13:58:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-26 14:16:26 +0200 |
| commit | 15999903f875f4b5dbb3d5240d2ca39acc3cd777 (patch) | |
| tree | 9906d3cf7d95d4d3f0e996811aa429532b825f0d /pretyping | |
| parent | d8176e6baaa33692ed82b9ac3c6e57e85f51dff0 (diff) | |
- 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.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1f462197c..940a54128 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 7b6fb262a..1b2afd19a 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 |