diff options
| author | herbelin | 2000-05-26 15:57:50 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-26 15:57:50 +0000 |
| commit | 2372cbdcabec698e5deb5abfc393ed3e6909995f (patch) | |
| tree | 57021a056665c433ca41aee125825bbeb7bc6d58 /kernel/type_errors.mli | |
| parent | b726fcfd1de249ab4fb5bb82f64fa349d2c17a0f (diff) | |
Modification messages d'erreurs, possibilité de n'importe quel constr dans les instances de références
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.mli')
| -rw-r--r-- | kernel/type_errors.mli | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 7ffbd312e8..a975419807 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -24,7 +24,9 @@ type type_error = | IllFormedBranch of constr * int * constr * constr | Generalization of (name * typed_type) * constr | ActualType of constr * constr * constr - | CantAply of string * unsafe_judgment * unsafe_judgment list + | CantApplyBadType of (int * constr * constr) + * unsafe_judgment * unsafe_judgment list + | CantApplyNonFunctional of 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 @@ -71,9 +73,12 @@ val error_generalization : val error_actual_type : path_kind -> env -> constr -> constr -> constr -> 'b -val error_cant_apply : - path_kind -> env -> string -> unsafe_judgment - -> unsafe_judgment list -> 'b +val error_cant_apply_not_functional : + path_kind -> env -> unsafe_judgment -> unsafe_judgment list -> 'b + +val error_cant_apply_bad_type : + path_kind -> env -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment list -> 'b val error_ill_formed_rec_body : path_kind -> env -> std_ppcmds |