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

3 files changed, 29 insertions, 9 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
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index 261bb0029c..435130ae6f 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -273,6 +273,7 @@ let rec xlate_match_pattern =
      CT_pattern_as
       (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
     | CPatOr (_,l) -> xlate_error "CPatOr: TODO"
+    | CPatRecord _ -> xlate_error "CPAtRecord: TODO"
     | CPatDelimiters(_, key, p) ->
 	CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
     | CPatPrim (_,Numeral n) ->
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 211d71a881..c47a1c4c4d 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -146,7 +146,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
       | _ ->
 	  if List.length k.cl_props <> 1 then
 	    errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body")
-	  else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props]
+	  else [Ident (dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props]
     in
       match k.cl_props with
       | [(na,b,ty)] ->
@@ -155,19 +155,35 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	  let c = interp_casted_constr_evars isevars env' term ty' in
 	    c :: subst
       | _ ->
+	  let get_id (idref, c) =
+	    match idref with
+	      | Ident id' -> id'
+	      | _ ->
+		  errorlabstrm "new_instance"
+		    (Pp.str "only local structures are managed")
+	  in
 	  let props, rest =
 	    List.fold_left
 	      (fun (props, rest) (id,_,_) ->
-		try
-		  let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
-		  let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
-		    Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
-		    c :: props, rest'
-		with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
+		 try
+		   let (loc_mid, c) =
+		     List.find (fun elt -> Name (snd (get_id elt)) = id) rest
+		   in
+		   let rest' =
+		     List.filter (fun elt -> Name (snd (get_id elt)) <> id) rest
+		   in
+		   match loc_mid with
+		     | Ident (loc, mid) ->
+			 Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+			 c :: props, rest'
+		     | _ -> errorlabstrm "new_instance"
+			 (Pp.str "only local structures are managed")
+		 with Not_found ->
+		   (CHole (Util.dummy_loc, None) :: props), rest)
 	      ([], props) k.cl_props
 	  in
 	    if rest <> [] then
-	      unbound_method env' k.cl_impl (fst (List.hd rest))
+	      unbound_method env' k.cl_impl (get_id (List.hd rest))
 	    else
 	      fst (type_ctx_instance isevars env' k.cl_props props subst)
   in