diff options
| author | Matthieu Sozeau | 2014-05-08 13:43:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-08 19:23:51 +0200 |
| commit | f912004bbe2c8f77de09cc290c3c687dc4ebf7f8 (patch) | |
| tree | eadad13bfd7e178d782bb46a9bd3e0daff84264b /checker/type_errors.ml | |
| parent | 0db1d850b940a5f2351c1ec6e26d1f8087064d40 (diff) | |
Adapt the checker to polymorphic universes and projections (untested).
Diffstat (limited to 'checker/type_errors.ml')
| -rw-r--r-- | checker/type_errors.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/type_errors.ml b/checker/type_errors.ml index e800ee3ef2..565005b908 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -45,7 +45,7 @@ type type_error = | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment | ReferenceVariables of constr - | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + | ElimArity of pinductive * sorts_family list * constr * unsafe_judgment * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of unsafe_judgment | WrongCaseInfo of inductive * case_info @@ -59,6 +59,7 @@ type type_error = | IllFormedRecBody of guard_error * name array * int | IllTypedRecBody of int * name array * unsafe_judgment array * constr array + | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error @@ -107,4 +108,5 @@ let error_ill_formed_rec_body env why lna i = let error_ill_typed_rec_body env i lna vdefj vargs = raise (TypeError (env, IllTypedRecBody (i,lna,vdefj,vargs))) - +let error_unsatisfied_constraints env c = + raise (TypeError (env, UnsatisfiedConstraints c)) |