diff options
| author | gmelquio | 2009-11-04 18:47:36 +0000 |
|---|---|---|
| committer | gmelquio | 2009-11-04 18:47:36 +0000 |
| commit | 208eceab14148fa561c36f71e2e1485e73832616 (patch) | |
| tree | 3763b73a349cca213cee543f8cf0204d65594ae6 /plugins/funind | |
| parent | fc7f18e8596a8b4e690ff726edb02a7cf319edbd (diff) | |
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
Fixed pretty printing of record syntax.
Allowed record syntax inside patterns. (Patch by Cedric Auger.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/indfun.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7cce53c7c3..68850603ba 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -626,7 +626,10 @@ let rec add_args id new_args b = CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2)) | CCast(loc,b1,CastCoerce) -> CCast(loc,add_args id new_args b1,CastCoerce) - | CRecord _ -> anomaly "add_args : CRecord" + | CRecord (loc, w, pars) -> + CRecord (loc, + (match w with Some w -> Some (add_args id new_args w) | _ -> None), + List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly "add_args : CNotation" | CGeneralization _ -> anomaly "add_args : CGeneralization" | CPrim _ -> b |