From dd279791aca531cd0f38ce79b675c68e08a4ff63 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 26 Aug 1999 16:26:54 +0000 Subject: environnement sur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@28 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/type_errors.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/type_errors.ml') diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 6949940a48..f99a026104 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))) -- cgit v1.2.3