diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-24 17:57:25 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-11-24 17:57:25 +0000 |
commit | be800056397163ec9c475e6aee44925c97f86f58 (patch) | |
tree | 373f85ebce6551ce9c3b4f876715fae44f5736b3 /kernel/type_errors.ml | |
parent | a67cb75db8dfd77dceefc8c40960b7e99ff6d302 (diff) |
MAJ pour fusion avec pretyping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/type_errors.ml')
-rw-r--r-- | kernel/type_errors.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index db992769d..eaef2dafc 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -28,6 +28,7 @@ type type_error = * typed_type array | NotInductive of constr | MLCase of string * constr * constr * constr * constr + | CantFindCaseType of constr exception TypeError of path_kind * context * type_error @@ -41,7 +42,7 @@ let error_not_type k env c = raise (TypeError (k, context env, NotAType c)) let error_assumption k env c = - raise (TypeError (k, context env, BadAssumption c)) + raise (TypeError (k, context env, BadAssumption c)) let error_reference_variables k env id = raise (TypeError (k, context env, ReferenceVariables id)) |