From 208eceab14148fa561c36f71e2e1485e73832616 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Wed, 4 Nov 2009 18:47:36 +0000
Subject: 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
---
 plugins/funind/indfun.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/funind')

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
-- 
cgit v1.2.3