diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-29 11:12:28 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-06-29 11:12:28 +0000 |
commit | 303a9cded85aa89c15d620d7a11e850c2ada7b37 (patch) | |
tree | 9ee4f95cdf005586855a4c60ab3d0b5dff99fd61 /kernel/type_errors.ml | |
parent | 43af153affecc21f87043ad96259039e20ed795f (diff) |
Normalisation des Evar avant génération des erreurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@527 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
-rw-r--r-- | kernel/type_errors.ml | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index a4661433e..d2891180a 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -11,8 +11,7 @@ open Environ type type_error = | UnboundRel of int - | CantExecute of constr - | NotAType of constr + | NotAType of unsafe_judgment | BadAssumption of constr | ReferenceVariables of identifier | ElimArity of inductive * constr list * constr * constr * constr @@ -20,7 +19,7 @@ type type_error = | CaseNotInductive of constr * constr | NumberBranches of constr * constr * int | IllFormedBranch of constr * int * constr * constr - | Generalization of (name * typed_type) * constr + | Generalization of (name * typed_type) * unsafe_judgment | ActualType of constr * constr * constr | CantApplyBadType of (int * constr * constr) * unsafe_judgment * unsafe_judgment list @@ -34,6 +33,7 @@ type type_error = | OccurCheck of int * constr | NotClean of int * constr | VarNotFound of identifier + | NotProduct of constr (* Pattern-matching errors *) | BadConstructor of constructor * inductive | WrongNumargConstructor of constructor_path * int @@ -42,11 +42,13 @@ type type_error = exception TypeError of path_kind * context * type_error -let error_unbound_rel k env n = - raise (TypeError (k, context env, UnboundRel n)) +let context_ise sigma env = + map_var_env (typed_app (Reduction.nf_ise1 sigma)) + (map_rel_env (typed_app (Reduction.nf_ise1 sigma)) + (context env)) -let error_cant_execute k env c = - raise (TypeError (k, context env, CantExecute c)) +let error_unbound_rel k env sigma n = + raise (TypeError (k, context_ise sigma env, UnboundRel n)) let error_not_type k env c = raise (TypeError (k, context env, NotAType c)) @@ -69,8 +71,8 @@ let error_number_branches k env c ct expn = let error_ill_formed_branch k env c i actty expty = raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty))) -let error_generalization k env nvar c = - raise (TypeError (k, context env, Generalization (nvar,c))) +let error_generalization k env sigma nvar c = + raise (TypeError (k, context_ise sigma env, Generalization (nvar,c))) let error_actual_type k env c actty expty = raise (TypeError (k, context env, ActualType (c,actty,expty))) @@ -78,8 +80,8 @@ let error_actual_type k env c actty expty = let error_cant_apply_not_functional k env rator randl = raise (TypeError (k, context env, CantApplyNonFunctional (rator,randl))) -let error_cant_apply_bad_type k env t rator randl = - raise (TypeError (k, context env, CantApplyBadType (t,rator,randl))) +let error_cant_apply_bad_type k env sigma t rator randl = + raise(TypeError (k, context_ise sigma env, CantApplyBadType (t,rator,randl))) let error_ill_formed_rec_body k env str lna i vdefs = raise (TypeError (k, context env, IllFormedRecBody (str,lna,i,vdefs))) @@ -92,3 +94,7 @@ let error_not_inductive k env c = let error_ml_case k env mes c ct br brt = raise (TypeError (k, context env, MLCase (mes,c,ct,br,brt))) + +let error_not_product env c = + raise (TypeError (CCI, context env, NotProduct c)) + |