diff options
author | 2003-09-02 10:14:10 +0000 | |
---|---|---|
committer | 2003-09-02 10:14:10 +0000 | |
commit | e78c38793e4fb98a5d9a1d951f49cd0c90cdb65f (patch) | |
tree | 736e5cfc7b56f088fbec56edf2753b5645209cb3 /interp/constrintern.ml | |
parent | f0660f6a814a7f8728a6cbb9fdd11499a8dbdca2 (diff) |
Plus de passage du scope tmp sous les lambdas
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4289 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r-- | interp/constrintern.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2fc5eaade..a1e9ae310 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -454,6 +454,9 @@ let rec subst_rawconstr loc interp subst (ids,impls,_,scopes as env) = function let set_type_scope (ids,impls,tmp_scope,scopes) = (ids,impls,Some Symbols.type_scope,scopes) +let reset_tmp_scope (ids,impls,tmp_scope,scopes) = + (ids,impls,None,scopes) + (**********************************************************************) (* Main loop *) @@ -499,10 +502,10 @@ let internalise sigma env allow_soapp lvar c = | CLambdaN (loc,[],c2) -> intern env c2 | CLambdaN (loc,(nal,ty)::bll,c2) -> - iterate_lam loc env ty (CLambdaN (loc, bll, c2)) nal + iterate_lam loc (reset_tmp_scope env) ty (CLambdaN (loc, bll, c2)) nal | CLetIn (loc,(_,na),c1,c2) -> - RLetIn (loc, na, intern (ids,impls,None,scopes) c1, - intern (name_fold Idset.add na ids,impls,tmp_scope,scopes) c2) + RLetIn (loc, na, intern (reset_tmp_scope env) c1, + intern (push_name_env env na) c2) | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) -> let scopes = option_cons tmp_scope scopes in Symbols.interp_numeral loc (Bignat.NEG p) scopes @@ -597,20 +600,18 @@ let internalise sigma env allow_soapp lvar c = let env_ids = List.fold_right Idset.add eqn_ids ids in (loc, eqn_ids,pl,intern (env_ids,impls,tmp_scope,scopes) rhs) - and iterate_prod loc2 (ids,impls,tmpsc,scopes as env) ty body = function + and iterate_prod loc2 env ty body = function | (loc1,na)::nal -> if nal <> [] then check_capture loc1 ty na; - let ids' = name_fold Idset.add na ids in - let body = iterate_prod loc2 (ids',impls,tmpsc,scopes) ty body nal in + let body = iterate_prod loc2 (push_name_env env na) ty body nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RProd (join_loc loc1 loc2, na, ty, body) | [] -> intern env body - and iterate_lam loc2 (ids,impls,tmpsc,scopes as env) ty body = function + and iterate_lam loc2 env ty body = function | (loc1,na)::nal -> if nal <> [] then check_capture loc1 ty na; - let ids' = name_fold Idset.add na ids in - let body = iterate_lam loc2 (ids',impls,tmpsc,scopes) ty body nal in + let body = iterate_lam loc2 (push_name_env env na) ty body nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RLambda (join_loc loc1 loc2, na, ty, body) | [] -> intern env body |