Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).

Thanks to Marc Lasson for the analysis of the problem and for the
initial patch.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13679 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 17 insertions, 10 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cbdb41ea38..e27bf67212 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -113,11 +113,11 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let outerl = [(ldots_var,inner)] in
       subst_rawvars outerl it
   | ALambda (na,ty,c) ->
-      let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c)
+      let e',na = g e na in RLambda (loc,na,Explicit,f e ty,f e' c)
   | AProd (na,ty,c) ->
-      let e,na = g e na in RProd (loc,na,Explicit,f e ty,f e c)
+      let e',na = g e na in RProd (loc,na,Explicit,f e ty,f e' c)
   | ALetIn (na,b,c) ->
-      let e,na = g e na in RLetIn (loc,na,f e b,f e c)
+      let e',na = g e na in RLetIn (loc,na,f e b,f e' c)
   | ACases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
@@ -135,18 +135,18 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
 	(loc,idl,patl,f e rhs)) eqnl in
       RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
-      let e,nal = list_fold_map g e nal in
-      let e,na = g e na in
-      RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
+      let e',nal = list_fold_map g e nal in
+      let e'',na = g e na in
+      RLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
   | AIf (c,(na,po),b1,b2) ->
-      let e,na = g e na in
-      RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
+      let e',na = g e na in
+      RIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | ARec (fk,idl,dll,tl,bl) ->
-      let e,idl = array_fold_map (to_id g) e idl in
       let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
 	  let e,na = g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
-      RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
+      let e',idl = array_fold_map (to_id g) e idl in
+      RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
   | ACast (c,k) -> RCast (loc,f e c,
 			  match k with
 			    | CastConv (k,t) -> CastConv (k,f e t)
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 661a8757a8..18e2479e50 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -59,3 +59,10 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end).
 Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).   
 Check [ 0 ].
 Check [ 0 # ; 1 ].
+
+(* Check well-scoping of alpha-renaming of private binders *)
+(* see bug #2248 (thanks to Marc Lasson) *)
+
+Notation "{ q , r | P }" := (fun (p:nat*nat), let (q, r) := p in P).
+Check (fun p, {q,r| q + r = p}).
+