Fix bug #2321, allowing "_" named projections in classes. Not realizing

the wish to allow named projections to not be put in the canonical
structures databases for Structures.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13474 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 12 insertions, 9 deletions

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 31e630741..1db9d407d 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -134,7 +134,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		  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);
+		    Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) 
+		      (List.assoc (Name mid) k.cl_projs);
 		    c :: props, rest'
 		with Not_found ->
 		  (CHole (Util.dummy_loc, None) :: props), rest
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b1cbed4af..bb25d0663 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -46,7 +46,7 @@ type typeclass = {
   cl_props : rel_context;
 
   (* The method implementaions as projections. *)
-  cl_projs : (identifier * constant option) list;
+  cl_projs : (name * constant option) list;
 }
 module Gmap = Fmap.Make(RefOrdered)
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 15cc95c93..871da5511 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -32,9 +32,10 @@ type typeclass = {
   (** Context of definitions and properties on defs, will not be shared *)
   cl_props : rel_context;
 
-  (** The methods implementations of the typeclass as projections. Some may be undefinable due to
-     sorting restrictions. *)
-  cl_projs : (identifier * constant option) list;
+  (** The methods implementations of the typeclass as projections. 
+      Some may be undefinable due to sorting restrictions or simply undefined if 
+      no name is provided. *)
+  cl_projs : (name * constant option) list;
 }
 
 type instance
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 09b983622..9418a4a5e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -212,7 +212,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 			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);
+			  Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) 
+			    (List.assoc (Name mid) k.cl_projs);
 			  c :: props, rest'
 		      with Not_found ->
 			(CHole (Util.dummy_loc, None) :: props), rest
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b751db85b..0822e6977 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -322,15 +322,15 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
 	Classes.set_typeclass_transparency (EvalConstRef cst) false;
 	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
-	cref, [proj_name, Some proj_cst]
+	cref, [Name proj_name, Some proj_cst]
     | _ ->
 	let idarg = Namegen.next_ident_away (snd id) (Termops.ids_of_context (Global.env())) in
 	let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
 	  params (Option.cata (fun x -> x) (Termops.new_Type ()) arity) fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
-	  IndRef ind, (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
-			     (List.rev fields) (Recordops.lookup_projections ind))
+	  IndRef ind, (List.map2 (fun (id, _, _) y -> (id, y))
+			 (List.rev fields) (Recordops.lookup_projections ind))
   in
   let ctx_context =
     List.map (fun (na, b, t) ->