diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-08-26 16:26:54 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-08-26 16:26:54 +0000 |
commit | dd279791aca531cd0f38ce79b675c68e08a4ff63 (patch) | |
tree | 32115bf156935bcb902d50fe3222e818ed692a1f /kernel/type_errors.ml | |
parent | 15ed739c91a22e91ae88d54215f6862fc1074a88 (diff) |
environnement sur
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@28 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
-rw-r--r-- | kernel/type_errors.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 6949940a4..f99a02610 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -21,13 +21,13 @@ type type_error = | NumberBranches of constr * constr * int | IllFormedBranch of constr * int * constr * constr | Generalization of (name * typed_type) * constr - | ActualType of unsafe_judgment * unsafe_judgment + | ActualType of constr * constr * constr | CantAply of string * unsafe_judgment * unsafe_judgment list | IllFormedRecBody of std_ppcmds * name list * int * constr array | IllTypedRecBody of int * name list * unsafe_judgment array * typed_type array -exception TypeError of path_kind * environment * type_error +exception TypeError of path_kind * context * type_error let error_unbound_rel k env n = raise (TypeError (k, context env, UnboundRel n)) @@ -59,8 +59,8 @@ let error_ill_formed_branch k env c i actty expty = let error_generalization k env nvar c = raise (TypeError (k, context env, Generalization (nvar,c))) -let error_actual_type k env cj tj = - raise (TypeError (k, context env, ActualType (cj,tj))) +let error_actual_type k env c actty expty = + raise (TypeError (k, context env, ActualType (c,actty,expty))) let error_cant_apply k env s rator randl = raise (TypeError (k, context env, CantAply (s,rator,randl))) |