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

14 files changed, 298 insertions, 99 deletions

diff --git a/CHANGES b/CHANGES
index 0c3d3603d9..152686e168 100644
--- a/CHANGES
+++ b/CHANGES
@@ -50,6 +50,7 @@ Language
 
 - Notations to names now behave like the names they refer to wrt implicit
   arguments and interpretation scopes.
+- Record syntax "{|x=...; y=...|}" now works inside patterns too.
 
 Vernacular commands
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 276c4c47a3..3aa42dbd85 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -182,6 +182,38 @@ of the chapter devoted to coercions.
 
 \Rem {\tt Structure} is a synonym of the keyword {\tt Record}.
 
+\Rem Creation of an object of record type can be done by calling {\ident$_0$}
+and passing arguments in the correct order.
+
+\begin{coq_example}
+Record point := { x : nat; y : nat }.
+Definition a := Build_point 5 3.
+\end{coq_example}
+
+The following syntax allows to create objects by using named fields. The
+fields do not have to be in any particular order, nor do they have to be all
+present if the missing ones can be inferred or prompted for (see
+Section~\ref{Program}).
+
+\begin{coq_example}
+Definition b := {| x := 5; y := 3 |}.
+Definition c := {| y := 3; x := 5 |}.
+\end{coq_example}
+
+This syntax can also be used for pattern matching.
+
+\begin{coq_example}
+Eval compute in (
+  match b with
+  | {| y := S n |} => n
+  | _ => 0
+  end).
+\end{coq_example}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
 \Rem An experimental syntax for projections based on a dot notation is
 available. The command to activate it is
 \begin{quote}
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0f3ed9511b..fc607e354b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -400,8 +400,25 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
   | PatCstr(loc,cstrsp,args,na) ->
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
-      let p = CPatCstr
-        (loc,extern_reference loc vars (ConstructRef cstrsp),args) in
+      let p =
+	try
+	  let projs = Recordops.lookup_projections (fst cstrsp) in
+	  let rec ip projs args acc =
+	    match projs with
+	      | [] -> acc
+	      | None :: q -> ip q args acc
+	      | Some c :: q ->
+		  match args with
+		    | [] -> raise No_match
+		    | CPatAtom(_, None) :: tail -> ip q tail acc
+			(* we don't want to have 'x = _' in our patterns *)
+		    | head :: tail -> ip q tail
+		        ((extern_reference loc Idset.empty (ConstRef c), head) :: acc)
+	    in
+	  CPatRecord(loc, List.rev (ip projs args []))
+	with
+	  Not_found | No_match ->
+	    CPatCstr (loc, extern_reference loc vars (ConstructRef cstrsp), args) in
       insert_pat_alias loc p na
 
 and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
@@ -619,9 +636,38 @@ let rec extern inctx scopes vars r =
 	     let subscopes = find_arguments_scope ref in
 	     let args =
 	       extern_args (extern true) (snd scopes) vars args subscopes in
-	     extern_app loc inctx (implicits_of_global ref)
-               (Some ref,extern_reference rloc vars ref)
-	       args
+	     begin
+	       try
+		 let cstrsp = match ref with ConstructRef c -> c | _ -> raise Not_found in
+		 let struc = Recordops.lookup_structure (fst cstrsp) in
+		 let projs = struc.Recordops.s_PROJ in
+		 let locals = struc.Recordops.s_PROJKIND in
+		 let rec cut args n =
+		   if n = 0 then args else cut (List.tl args) (n - 1) in
+		 let args = cut args struc.Recordops.s_EXPECTEDPARAM in
+		 let rec ip projs locs args acc =
+		   match projs with
+		     | [] -> acc
+		     | None :: q -> raise No_match
+		     | Some c :: q ->
+		         match locs with
+			   | [] -> anomaly "projections corruption [Constrextern.extern]"
+			   | (_, false) :: locs' ->
+			       (* we don't want to print locals *)
+			       ip q locs' args acc
+			   | (_, true) :: locs' ->
+			       match args with
+				 | [] -> raise No_match
+				     (* we give up since the constructor is not complete *)
+				 | head :: tail -> ip q locs' tail
+				     ((extern_reference loc Idset.empty (ConstRef c), head) :: acc)
+		   in
+		 CRecord (loc, None, List.rev (ip projs locals args []))
+	       with
+		 | Not_found | No_match ->
+		     extern_app loc inctx (implicits_of_global ref)
+		       (Some ref,extern_reference rloc vars ref) args
+	     end
 	 | _       ->
 	     explicitize loc inctx [] (None,sub_extern false scopes vars f)
                (List.map (sub_extern true scopes vars) args))
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 299f742d1a..0f593e67c3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -47,6 +47,38 @@ let for_grammar f x =
     a
 
 (**********************************************************************)
+(* Locating reference, possibly via an abbreviation *)
+
+let locate_reference qid =
+  match Nametab.locate_extended qid with
+    | TrueGlobal ref -> ref
+    | SynDef kn ->
+	match Syntax_def.search_syntactic_definition dummy_loc kn with
+	  | [],ARef ref -> ref
+	  | _ -> raise Not_found
+
+let is_global id =
+  try
+    let _ = locate_reference (qualid_of_ident id) in true
+  with Not_found ->
+    false
+
+let global_reference_of_reference ref =
+  locate_reference (snd (qualid_of_reference ref))
+
+let global_reference id =
+  constr_of_global (locate_reference (qualid_of_ident id))
+
+let construct_reference ctx id =
+  try
+    Term.mkVar (let _ = Sign.lookup_named id ctx in id)
+  with Not_found ->
+    global_reference id
+
+let global_reference_in_absolute_module dir id =
+  constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
+
+(**********************************************************************)
 (* Internalisation errors                                             *)
 
 type internalisation_error =
@@ -607,12 +639,105 @@ let mustbe_constructor loc ref f aliases patl scopes =
   with (Environ.NotEvaluableConst _ | Not_found) ->
     raise (InternalisationError (loc,NotAConstructor ref))
 
+let sort_fields mode loc l completer =
+(*mode=false if pattern and true if constructor*)
+  match l with
+    | [] -> None
+    | (refer, value)::rem ->
+	let (nparams,          (* the number of parameters *)
+	     base_constructor, (* the reference constructor of the record *)
+	     (max,             (* number of params *)
+	      (first_index,    (* index of the first field of the record *)
+	       list_proj)))    (* list of projections *)
+	  =
+	  let record =
+	    try Recordops.find_projection
+	      (global_reference_of_reference refer)
+	    with Not_found ->
+	      user_err_loc (loc, "intern", str"Not a projection")
+	    in
+	  (* elimination of the first field from the projections *)
+	  let rec build_patt l m i acc =
+	    match l with
+	      | [] -> (i, acc)
+	      | (Some name) :: b->
+		 (match m with
+		    | [] -> anomaly "Number of projections mismatch"
+		    | (_, regular)::tm ->
+		       let boolean = not regular in
+		       if ConstRef name = global_reference_of_reference refer
+		       then
+			 if boolean && mode then
+			   user_err_loc (loc, "", str"No local fields allowed in a record construction.")
+			 else build_patt b tm (i + 1) (i, snd acc) (* we found it *)
+		       else
+			  build_patt b tm (if boolean&&mode then i else i + 1)
+			    (if boolean && mode then acc
+			     else fst acc, (i, ConstRef name) :: snd acc))
+	      | None :: b-> (* we don't want anonymous fields *)
+		 if mode then
+		   user_err_loc (loc, "", str "This record contains anonymous fields.")
+		 else build_patt b m (i+1) acc
+		   (* anonymous arguments don't appear in m *)
+	    in
+	  let ind = record.Recordops.s_CONST in
+	  try (* insertion of Constextern.reference_global *)
+	    (record.Recordops.s_EXPECTEDPARAM,
+	     Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef ind)),
+	     build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[]))
+	  with Not_found -> anomaly "Environment corruption for records."
+	  in
+	(* now we want to have all fields of the pattern indexed by their place in
+	   the constructor *)
+	let rec sf patts accpatt =
+	  match patts with
+	    | [] -> accpatt
+	    | p::q->
+	       let refer, patt = p in
+	       let rec add_patt l acc =
+		 match l with
+		   | [] ->
+		       user_err_loc
+			 (loc, "",
+			  str "This record contains fields of different records.")
+		   | (i, a) :: b->
+		       if global_reference_of_reference refer = a
+		       then (i,List.rev_append acc l)
+		       else add_patt b ((i,a)::acc)
+	         in
+	       let (index, projs) = add_patt (snd accpatt) [] in
+		 sf q ((index, patt)::fst accpatt, projs) in
+	let (unsorted_indexed_pattern, remainings) =
+	  sf rem ([first_index, value], list_proj) in
+	(* we sort them *)
+	let sorted_indexed_pattern =
+	  List.sort (fun (i, _) (j, _) -> compare i j) unsorted_indexed_pattern in
+	(* a function to complete with wildcards *)
+	let rec complete_list n l =
+	  if n <= 1 then l else complete_list (n-1) (completer n l) in
+	(* a function to remove indice *)
+	let rec clean_list l i acc =
+	  match l with
+	    | [] -> complete_list (max - i) acc
+	    | (k, p)::q-> clean_list q k (p::(complete_list (k - i) acc))
+	  in
+	Some (nparams, base_constructor,
+	  List.rev (clean_list sorted_indexed_pattern 0 []))
+
 let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
   let intern_pat = intern_cases_pattern genv in
   match pat with
   | CPatAlias (loc, p, id) ->
       let aliases' = merge_aliases aliases id in
       intern_pat scopes aliases' tmp_scope p
+    | CPatRecord (loc, l) ->
+	let sorted_fields = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in
+	let self_patt =
+	  match sorted_fields with
+	    | None -> CPatAtom (loc, None)
+	    | Some (_, head, pl) -> CPatCstr(loc, head, pl)
+	  in
+	intern_pat scopes aliases tmp_scope self_patt
   | CPatCstr (loc, head, pl) ->
       let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl scopes in
       check_constructor_length genv loc c idslpl1 pl2;
@@ -973,39 +1098,19 @@ let internalise sigma globalenv env allow_patvar lvar c =
           (* Now compact "(f args') args" *)
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
-    | CRecord (loc, w, fs) ->
-	let id, _ = List.hd fs in
-	let record =
-	  let (id,_,_,_),_ = intern_applied_reference intern env lvar [] (Ident id) in
-	    match id with
-	    | RRef (loc, ref) ->
-		(try Recordops.find_projection ref
-		  with Not_found -> user_err_loc (loc, "intern", str"Not a projection"))
-	    | c -> user_err_loc (loc_of_rawconstr id, "intern", str"Not a projection")
-	in
-	let args =
-	  let pars = list_make record.Recordops.s_EXPECTEDPARAM (CHole (loc, None)) in
-	  let fields, rest =
-	    List.fold_left (fun (args, rest as acc) (na, b) ->
-	      if b then
-		try
-		  let id = out_name na in
-		  let _, t = List.assoc id rest in
-		    t :: args, List.remove_assoc id rest
-		with _ -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: args, rest
-	      else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) fs) record.Recordops.s_PROJKIND
+    | CRecord (loc, _, fs) ->
+	let cargs =
+	  sort_fields true loc fs
+	    (fun k l -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: l)
 	  in
-	    if rest <> [] then
-	      let id, (loc, t) = List.hd rest in
-		user_err_loc (loc,"intern",(str "Unknown field name " ++ pr_id id))
-	    else pars @ List.rev fields
-	in
-	let constrname =
-	  Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef record.Recordops.s_CONST))
-	in
-	let app = CAppExpl (loc, (None, constrname), args) in
+	begin
+	  match cargs with
+	    | None -> user_err_loc (loc, "intern", str"No constructor inference.")
+	    | Some (n, constrname, args) ->
+		let pars = list_make n (CHole (loc, None)) in
+		let app = CAppExpl (loc, (None, constrname), List.rev_append pars args) in
 	  intern env app
-
+	end
     | CCases (loc, sty, rtnpo, tms, eqns) ->
         let tms,env' = List.fold_right
           (fun citm (inds,env) ->
@@ -1372,33 +1477,3 @@ let interp_context_evars ?(fail_anonymous=false) evdref env params =
   let bl = intern_context fail_anonymous !evdref env params in
     interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t)
       (Default.understand_judgment_tcc evdref) env bl
-
-(**********************************************************************)
-(* Locating reference, possibly via an abbreviation *)
-
-let locate_reference qid =
-  match Nametab.locate_extended qid with
-    | TrueGlobal ref -> ref
-    | SynDef kn ->
-	match Syntax_def.search_syntactic_definition dummy_loc kn with
-	  | [],ARef ref -> ref
-	  | _ -> raise Not_found
-
-let is_global id =
-  try
-    let _ = locate_reference (qualid_of_ident id) in true
-  with Not_found ->
-    false
-
-let global_reference id =
-  constr_of_global (locate_reference (qualid_of_ident id))
-
-let construct_reference ctx id =
-  try
-    Term.mkVar (let _ = Sign.lookup_named id ctx in id)
-  with Not_found ->
-    global_reference id
-
-let global_reference_in_absolute_module dir id =
-  constr_of_global (Nametab.global_of_path (Libnames.make_path dir id))
-
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ec1b20a12b..04715d51b3 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -634,6 +634,7 @@ type cases_pattern_expr =
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
   | CPatPrim of loc * prim_token
+  | CPatRecord of loc * (reference * cases_pattern_expr) list
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
@@ -647,7 +648,7 @@ type constr_expr =
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) *
       (constr_expr * explicitation located option) list
-  | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
+  | CRecord of loc * constr_expr option * (reference * constr_expr) list
   | CCases of loc * case_style * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
@@ -743,6 +744,7 @@ let cases_pattern_expr_loc = function
   | CPatAtom (loc,_) -> loc
   | CPatOr (loc,_) -> loc
   | CPatNotation (loc,_,_) -> loc
+  | CPatRecord (loc, _) -> loc
   | CPatPrim (loc,_) -> loc
   | CPatDelimiters (loc,_,_) -> loc
 
@@ -774,6 +776,8 @@ let is_constructor id =
   with Not_found -> true
 
 let rec cases_pattern_fold_names f a = function
+  | CPatRecord (_, l) ->
+      List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
   | CPatAlias (_,pat,id) -> f id a
   | CPatCstr (_,_,patl) | CPatOr (_,patl) ->
       List.fold_left (cases_pattern_fold_names f) a patl
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 2c28b3bead..1966bf552c 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -120,6 +120,7 @@ type cases_pattern_expr =
   | CPatOr of loc * cases_pattern_expr list
   | CPatNotation of loc * notation * cases_pattern_expr notation_substitution
   | CPatPrim of loc * prim_token
+  | CPatRecord of Util.loc * (reference * cases_pattern_expr) list
   | CPatDelimiters of loc * string * cases_pattern_expr
 
 type constr_expr =
@@ -133,7 +134,7 @@ type constr_expr =
   | CAppExpl of loc * (proj_flag * reference) * constr_expr list
   | CApp of loc * (proj_flag * constr_expr) *
       (constr_expr * explicitation located option) list
-  | CRecord of loc * constr_expr option * (identifier located * constr_expr) list
+  | CRecord of loc * constr_expr option * (reference * constr_expr) list
   | CCases of loc * case_style * constr_expr option *
       (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list located list * constr_expr) list
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 (
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
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5d3180ff7b..0af25666d4 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -30,6 +30,11 @@ type struc_typ = {
 val declare_structure :
   inductive * constructor * (name * bool) list * constant option list -> unit
 
+(* [lookup_structure isp] returns the struc_typ associated to the
+   inductive path [isp] if it corresponds to a structure, otherwise
+   it fails with [Not_found] *)
+val lookup_structure : inductive -> struc_typ
+
 (* [lookup_projections isp] returns the projections associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
    it fails with [Not_found] *)
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 07de95d8ec..67b699782c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1035,17 +1035,17 @@ let require_library dirpath =
 let declare_instance_refl binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
   in anew_instance binders instance
-       [((dummy_loc,id_of_string "reflexivity"),lemma)]
+       [(Ident (dummy_loc,id_of_string "reflexivity"),lemma)]
 
 let declare_instance_sym binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance binders instance
-       [((dummy_loc,id_of_string "symmetry"),lemma)]
+       [(Ident (dummy_loc,id_of_string "symmetry"),lemma)]
 
 let declare_instance_trans binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
   in anew_instance binders instance
-       [((dummy_loc,id_of_string "transitivity"),lemma)]
+       [(Ident (dummy_loc,id_of_string "transitivity"),lemma)]
 
 let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyConstructor (false,None)))
 
@@ -1070,16 +1070,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
 	    anew_instance binders instance
-	      [((dummy_loc,id_of_string "PreOrder_Reflexive"), lemma1);
-	       ((dummy_loc,id_of_string "PreOrder_Transitive"),lemma3)])
+	      [(Ident (dummy_loc,id_of_string "PreOrder_Reflexive"), lemma1);
+	       (Ident (dummy_loc,id_of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) ->
 	let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
 	    anew_instance binders instance
-	      [((dummy_loc,id_of_string "PER_Symmetric"), lemma2);
-	       ((dummy_loc,id_of_string "PER_Transitive"),lemma3)])
+	      [(Ident (dummy_loc,id_of_string "PER_Symmetric"), lemma2);
+	       (Ident (dummy_loc,id_of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) ->
 	let _lemma_refl = declare_instance_refl binders a aeq n lemma1 in
 	let _lemma_sym = declare_instance_sym binders a aeq n lemma2 in
@@ -1087,9 +1087,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
 	  anew_instance binders instance
-	    [((dummy_loc,id_of_string "Equivalence_Reflexive"), lemma1);
-	     ((dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2);
-	     ((dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)])
+	    [(Ident (dummy_loc,id_of_string "Equivalence_Reflexive"), lemma1);
+	     (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2);
+	     (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)])
 
 type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
@@ -1267,9 +1267,9 @@ let add_setoid binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance binders instance
-      [((dummy_loc,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       ((dummy_loc,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       ((dummy_loc,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+      [(Ident (dummy_loc,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+       (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+       (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
 let add_morphism_infer glob m n =
   init_setoid ();
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 7fdd6bd7e4..de2e78ba54 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -200,7 +200,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	  | _ ->
 	      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
 	let subst =
 	  match k.cl_props with
@@ -211,12 +211,18 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	      let c = interp_casted_constr_evars evars env' term ty' in
 		c :: subst
 	  | _ ->
+	      let get_id =
+		function
+		  | Ident id' -> id'
+		  | _ -> errorlabstrm "new_instance" (Pp.str "Only local structures are handled")
+	        in
 	      let props, rest =
 		List.fold_left
 		  (fun (props, rest) (id,b,_) ->
 		    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
+		      let (loc_mid, c) = List.find (fun (id', _) -> Name (snd (get_id id')) = id) rest in
+		      let rest' = List.filter (fun (id', _) -> Name (snd (get_id id')) <> id) rest in
+		      let (loc, mid) = get_id loc_mid in
 			Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
 			c :: props, rest'
 		    with Not_found ->
@@ -224,7 +230,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 		  ([], 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 (fst (List.hd rest)))
 		else
 		  type_ctx_instance evars env' k.cl_props props subst
 	in