diff options
| author | herbelin | 2010-12-04 15:06:00 +0000 |
|---|---|---|
| committer | herbelin | 2010-12-04 15:06:00 +0000 |
| commit | 2b6ce061e6c9170bdaf74633edc8323512f1d456 (patch) | |
| tree | 82e5c8c53d21a46b17c59905dc3fd3e05ce64226 /interp | |
| parent | aea34fdc7caec6faf9cf54e70ae33631357ec0f1 (diff) | |
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
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/topconstr.ml | 20 |
1 files changed, 10 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) |