diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-24 13:39:23 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-24 13:39:23 +0000 |
commit | 3afaf3dde673d77cacaabc354f008dfbe49a7cee (patch) | |
tree | 4264164faf763ab8d18274cd5aeffe5a1de21728 /pretyping/pretype_errors.ml | |
parent | 83f038e61a4424fcf71aada9f97c91165b73aef8 (diff) |
Passage à des contextes de vars et de rels pouvant contenir des déclarations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretype_errors.ml')
-rw-r--r-- | pretyping/pretype_errors.ml | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 9f711f390..247620a67 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -11,51 +11,51 @@ let raise_pretype_error (loc,k,ctx,te) = Stdpp.raise_with_loc loc (TypeError(k,ctx,te)) let error_var_not_found_loc loc k s = - raise_pretype_error (loc,k, Global.context() (*bidon*), VarNotFound s) + raise_pretype_error (loc,k, Global.env() (*bidon*), VarNotFound s) let error_cant_find_case_type_loc loc env expr = - raise_pretype_error (loc, CCI, context env, CantFindCaseType expr) + raise_pretype_error (loc, CCI, env, CantFindCaseType expr) let error_actual_type_loc loc env c actty expty = - raise_pretype_error (loc, CCI, context env, ActualType (c,actty,expty)) + raise_pretype_error (loc, CCI, env, ActualType (c,actty,expty)) let error_cant_apply_not_functional_loc loc env rator randl = raise_pretype_error - (loc,CCI,context env, CantApplyNonFunctional (rator,randl)) + (loc,CCI,env, CantApplyNonFunctional (rator,randl)) let error_cant_apply_bad_type_loc loc env t rator randl = - raise_pretype_error (loc, CCI, context env, CantApplyBadType (t,rator,randl)) + raise_pretype_error (loc, CCI, env, CantApplyBadType (t,rator,randl)) let error_ill_formed_branch k env c i actty expty = - raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty))) + raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty))) let error_number_branches_loc loc k env c ct expn = - raise_pretype_error (loc, k, context env, NumberBranches (c,ct,expn)) + raise_pretype_error (loc, k, env, NumberBranches (c,ct,expn)) let error_case_not_inductive_loc loc k env c ct = - raise_pretype_error (loc, k, context env, CaseNotInductive (c,ct)) + raise_pretype_error (loc, k, env, CaseNotInductive (c,ct)) (* Pattern-matching errors *) let error_bad_constructor_loc loc k cstr ind = - raise_pretype_error (loc, k, Global.context(), BadConstructor (cstr,ind)) + raise_pretype_error (loc, k, Global.env(), BadConstructor (cstr,ind)) let error_wrong_numarg_constructor_loc loc k c n = - raise_pretype_error (loc, k, Global.context(), WrongNumargConstructor (c,n)) + raise_pretype_error (loc, k, Global.env(), WrongNumargConstructor (c,n)) let error_wrong_predicate_arity_loc loc k env c n1 n2 = - raise_pretype_error (loc, k, context env, WrongPredicateArity (c,n1,n2)) + raise_pretype_error (loc, k, env, WrongPredicateArity (c,n1,n2)) let error_needs_inversion k env x t = - raise (TypeError (k, context env, NeedsInversion (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, context env, IllFormedBranch (c,i,actty,expty)) + raise_pretype_error (loc, k, env, IllFormedBranch (c,i,actty,expty)) let error_occur_check k env ev c = - raise (TypeError (k, context env, OccurCheck (ev,c))) + raise (TypeError (k, env, OccurCheck (ev,c))) let error_not_clean k env ev c = - raise (TypeError (k, context env, NotClean (ev,c))) + raise (TypeError (k, env, NotClean (ev,c))) |