diff options
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 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 |