diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-06 12:46:25 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-09-06 12:46:25 +0000 |
commit | 8ec12027e4641f88272c0275e31e93565f7c34cc (patch) | |
tree | 06d90a5a2532cc1c2b7b43e1229e5257c3b58970 /pretyping/pretype_errors.ml | |
parent | 1c8eaac415b43ec27aa81afdc39837c14fb2d92c (diff) |
kernel/type_errors.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@583 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretype_errors.ml')
-rw-r--r-- | pretyping/pretype_errors.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 247620a67..b8a080366 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -49,13 +49,16 @@ let error_wrong_predicate_arity_loc loc k env c n1 n2 = let error_needs_inversion k env x t = raise (TypeError (k, env, NeedsInversion (x,t))) - let error_ill_formed_branch_loc loc k env c i actty expty = raise_pretype_error (loc, k, env, IllFormedBranch (c,i,actty,expty)) +(*s Implicit arguments synthesis errors *) + +let error_unexpected_type_loc loc env actty expty = + raise_pretype_error (loc, CCI, env, UnexpectedType (actty, expty)) + let error_occur_check k env ev c = raise (TypeError (k, env, OccurCheck (ev,c))) let error_not_clean k env ev c = raise (TypeError (k, env, NotClean (ev,c))) - |