From e78c38793e4fb98a5d9a1d951f49cd0c90cdb65f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 Sep 2003 10:14:10 +0000
Subject: 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
---
 interp/constrextern.ml |  2 +-
 interp/constrintern.ml | 19 ++++++++++---------
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0119430aba..58869667b8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -564,7 +564,7 @@ and factorize_lambda inctx scopes vars aty = function
 	-> let (nal,c) =
 	     factorize_lambda inctx scopes (add_vname vars na) aty c in
            ((loc,na)::nal,c)
-  | c -> ([],extern inctx scopes vars c)
+  | c -> ([],sub_extern inctx scopes vars c)
 
 and extern_eqn inctx scopes vars (loc,ids,pl,c) =
   (loc,List.map (extern_cases_pattern_in_scope (snd scopes) vars) pl,
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2fc5eaade6..a1e9ae3109 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
-- 
cgit v1.2.3