diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /kernel/type_errors.ml | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'kernel/type_errors.ml')
-rw-r--r-- | kernel/type_errors.ml | 33 |
1 files changed, 18 insertions, 15 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 0a920e40..33c4172e 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,7 +8,6 @@ open Names open Term -open Sign open Environ open Reduction @@ -31,6 +30,7 @@ type guard_error = | RecCallInCaseArg of constr | RecCallInCasePred of constr | NotGuardedForm of constr + | ReturnPredicateNotCoInductive of constr type arity_error = | NonInformativeToInformative @@ -42,26 +42,27 @@ type type_error = | UnboundVar of variable | NotAType of unsafe_judgment | BadAssumption of unsafe_judgment - | ReferenceVariables of constr - | ElimArity of inductive * sorts_family list * constr * unsafe_judgment + | ReferenceVariables of identifier * constr + | 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 + | WrongCaseInfo of pinductive * case_info | NumberBranches of unsafe_judgment * int - | IllFormedBranch of constr * constructor * constr * constr - | Generalization of (name * types) * unsafe_judgment + | IllFormedBranch of constr * pconstructor * constr * constr + | Generalization of (Name.t * types) * unsafe_judgment | ActualType of unsafe_judgment * types | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment array | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment array - | IllFormedRecBody of guard_error * name array * int * env * unsafe_judgment array + | IllFormedRecBody of guard_error * Name.t array * int * env * unsafe_judgment array | IllTypedRecBody of - int * name array * unsafe_judgment array * types array + int * Name.t array * unsafe_judgment array * types array + | UnsatisfiedConstraints of Univ.constraints exception TypeError of env * type_error -let nfj {uj_val=c;uj_type=ct} = - {uj_val=c;uj_type=nf_betaiota ct} +let nfj env {uj_val=c;uj_type=ct} = + {uj_val=c;uj_type=nf_betaiota env ct} let error_unbound_rel env n = raise (TypeError (env, UnboundRel n)) @@ -75,8 +76,8 @@ let error_not_type env j = let error_assumption env j = raise (TypeError (env, BadAssumption j)) -let error_reference_variables env id = - raise (TypeError (env, ReferenceVariables id)) +let error_reference_variables env id c = + raise (TypeError (env, ReferenceVariables (id,c))) let error_elim_arity env ind aritylst c pj okinds = raise (TypeError (env, ElimArity (ind,aritylst,c,pj,okinds))) @@ -85,11 +86,11 @@ let error_case_not_inductive env j = raise (TypeError (env, CaseNotInductive j)) let error_number_branches env cj expn = - raise (TypeError (env, NumberBranches (nfj cj,expn))) + raise (TypeError (env, NumberBranches (nfj env cj,expn))) let error_ill_formed_branch env c i actty expty = raise (TypeError (env, - IllFormedBranch (c,i,nf_betaiota actty, nf_betaiota expty))) + IllFormedBranch (c,i,nf_betaiota env actty, nf_betaiota env expty))) let error_generalization env nvar c = raise (TypeError (env, Generalization (nvar,c))) @@ -115,3 +116,5 @@ let error_elim_explain kp ki = | InType, InSet -> StrongEliminationOnNonSmallType (* if Set impredicative *) | _ -> WrongArity +let error_unsatisfied_constraints env c = + raise (TypeError (env, UnsatisfiedConstraints c)) |