diff options
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 |