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

2 files changed, 14 insertions, 5 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7e2b41926c..669d1f2aec 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -239,7 +239,7 @@ GEXTEND Gram
     ] ]
   ;
   record_field_declaration:
-    [ [ id = identref; params = LIST0 identref; ":="; c = lconstr ->
+    [ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
       (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
   ;
   binder_constr:
@@ -342,6 +342,9 @@ GEXTEND Gram
     [ [ pll = LIST1 mult_pattern SEP "|";
         "=>"; rhs = lconstr -> (loc,pll,rhs) ] ]
   ;
+  recordpattern:
+    [ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
+  ;
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
@@ -360,6 +363,7 @@ GEXTEND Gram
       [ c = pattern; "%"; key=IDENT -> CPatDelimiters (loc,key,c) ]
     | "0"
       [ r = Prim.reference -> CPatAtom (loc,Some r)
+      | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (loc, pat)
       | "_" -> CPatAtom (loc,None)
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 80e1eb144d..4fd7390e81 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -171,9 +171,14 @@ let pr_evar pr n l =
 
 let las = lapp
 let lpator = 100
+let lpatrec = 0
 
 let rec pr_patt sep inh p =
   let (strm,prec) = match p with
+  | CPatRecord (_, l) ->
+      let pp (c, p) =
+	pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p in
+      str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec
   | CPatAlias (_,p,id) ->
       pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las
   | CPatCstr (_,c,[]) -> pr_reference c, latom
@@ -565,10 +570,10 @@ let pr pr sep inherited a =
 	| None -> spc ()
 	| Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc ()
       in
-	hv 0 (str"{" ++ beg ++
-		 prlist_with_sep (fun () -> spc () ++ str";" ++ spc ())
-		 (fun ((_,id), c) -> pr_id id ++ spc () ++ str":=" ++ spc () ++ pr spc ltop c)
-		 l), latom
+	hv 0 (str"{|" ++ beg ++
+	      prlist_with_sep pr_semicolon
+		(fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l
+	      ++ str" |}"), latom
 
   | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) ->
       hv 0 (