diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-13 13:19:46 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-13 13:19:46 +0000 |
| commit | 45f4f60d92bd80f78713b68888b31d37f4134238 (patch) | |
| tree | 78f10ce2f28f8abcc3cc68d0af4dda2a7da2edd3 /pretyping | |
| parent | 338dd533c27374771b0e880dcb74fba972dc79f1 (diff) | |
Ajout map_rawconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3126 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 15 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 |
2 files changed, 17 insertions, 0 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 8e46a41b2..43bd6fc5b 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -90,6 +90,21 @@ type rawconstr = - boolean in POldCase means it is recursive i*) +let map_rawconstr f = function + | RVar (loc,id) -> RVar (loc,id) + | RApp (loc,g,args) -> RApp (loc,f g, List.map f args) + | RLambda (loc,na,ty,c) -> RLambda (loc,na,f ty,f c) + | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c) + | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c) + | RCases (loc,prinfo,tyopt,tml,pl) -> + RCases (loc,prinfo,option_app f tyopt,List.map f tml, + List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl) + | ROldCase (loc,b,tyopt,tm,bv) -> + ROldCase (loc,b,option_app f tyopt,f tm, Array.map f bv) + | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv) + | RCast (loc,c,t) -> RCast (loc,f c,f t) + | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _ | RDynamic _) as x -> x + let rec subst_pat subst pat = match pat with | PatVar _ -> pat diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 04cd4da2a..51ea18028 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -90,6 +90,8 @@ type rawconstr = - option in PHole tell if the "?" was apparent or has been implicitely added i*) +val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr + val dummy_loc : loc val loc_of_rawconstr : rawconstr -> loc val join_loc : loc -> loc -> loc |