diff options
| author | filliatr | 1999-08-26 16:26:54 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-26 16:26:54 +0000 |
| commit | dd279791aca531cd0f38ce79b675c68e08a4ff63 (patch) | |
| tree | 32115bf156935bcb902d50fe3222e818ed692a1f /kernel/type_errors.mli | |
| 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.mli')
| -rw-r--r-- | kernel/type_errors.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index cec8b78184..76bf18cc32 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -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 val error_unbound_rel : path_kind -> 'a unsafe_env -> int -> 'b @@ -56,7 +56,7 @@ val error_generalization : path_kind -> 'a unsafe_env -> name * typed_type -> constr -> 'b val error_actual_type : - path_kind -> 'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> 'b + path_kind -> 'a unsafe_env -> constr -> constr -> constr -> 'b val error_cant_apply : path_kind -> 'a unsafe_env -> string -> unsafe_judgment |