Fix bugs that were reopened due to the change of setoid

implementation. Mostly syntax changes when declaring parametric
relations, but also some declarations were relying on "default"
relations on some carrier. Added a new DefaultRelation type class that
allows to do that, falling back to the last declared Equivalence
relation by default. This will be bound to Add Relation in the next
commit. 

Also, move the "left" and "right" notations in Program.Utils to "in_left" and
"in_right" to avoid clashes with existing scripts.

Minor change to record to allow choosing the name of the argument for
the record in projections to avoid possible incompatibilities.


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

3 files changed, 8 insertions, 8 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 32803742a0..4af59ff621 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -185,7 +185,8 @@ let declare_structure env id idbuild params arity fields =
       mind_entry_inds = [mie_ind] } in
   let kn = Command.declare_mutual_with_eliminations true mie in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
-  let kinds,sp_projs = Record.declare_projections rsp (List.map (fun _ -> false) fields) fields in
+  let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
+  let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in
   let _build = ConstructRef (rsp,1) in
     Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
     rsp
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b94dffe1a0..b045573045 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -131,15 +131,14 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
   substl_rel_context (subst@[mkInd indsp]) fields
 
 (* We build projections *)
-let declare_projections indsp coers fields =
+let declare_projections indsp ?name coers fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let paramdecls = mib.mind_params_ctxt in
   let r = mkInd indsp in
   let rp = applist (r, extended_rel_list 0 paramdecls) in
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
-  let x = Name (next_ident_away mip.mind_typename (ids_of_context (Global.env()))) in
-    (* Termops.named_hd (Global.env()) r Anonymous  *)
+  let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in
   let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
   let lifted_fields = lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
diff --git a/toplevel/record.mli b/toplevel/record.mli
index e322dcfd0b..5ba8b04e1a 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -16,12 +16,12 @@ open Vernacexpr
 open Topconstr
 (*i*)
 
-(* [declare_projections ref coers params fields] declare projections of
-   record [ref] (if allowed), and put them as coercions accordingly to
-   [coers]; it returns the absolute names of projections *)
+(* [declare_projections ref name coers params fields] declare projections of
+   record [ref] (if allowed) using the given [name] as argument, and put them
+   as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> bool list -> rel_context -> bool list * constant option list
+  inductive -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
 
 val definition_structure :
   lident with_coercion * local_binder list *