Fixes in handling of implicit arguments:

- Now [ id : Class foo ] makes id an explicit argument, 
  and [ Class foo ] is equivalent to [ {someid} : Class foo ].
  This makes declarations such as "Class Ord [ eq : Eq a ]" have
  sensible implicit args.
- Better handling of {} in class and record declarations, refactorize 
  code for declaring structures and classes.  
- Fix merging of implicit arguments information on section closing.


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

25 files changed, 231 insertions, 186 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 54abacaf6..6c09e4ace 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -696,11 +696,9 @@ let intern_typeclass_binders intern_type lvar env bl =
 	(env, (na,bk,None,ty)::bl))
     env bl
 
-let intern_typeclass_binder intern_type lvar (env,bl) na b ty =
-  let ctx = (na, b, ty) in
-  let (fvs, bind) = Implicit_quantifiers.generalize_class_binders_raw (pi1 env) [ctx] in
-  let env, ifvs = intern_typeclass_binders intern_type lvar (env,bl) fvs in
-    intern_typeclass_binders intern_type lvar (env,ifvs) bind
+let intern_typeclass_binder intern_type lvar (env,bl) cb =
+  let (ids, fvs, bind) = Implicit_quantifiers.generalize_class_binder_raw (pi1 env) cb in
+    intern_typeclass_binders intern_type lvar (env,bl) (fvs@[bind])
     
 let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = function
   | LocalRawAssum(nal,bk,ty) ->
@@ -713,8 +711,8 @@ let intern_local_binder_aux intern intern_type lvar ((ids,ts,sc as env),bl) = fu
 		(fun ((ids,ts,sc),bl) (_,na) ->
 		  ((name_fold Idset.add na ids,ts,sc), (na,k,None,ty)::bl))
 		(env,bl) nal
-	| TypeClass b ->
-	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal) b ty)
+	| TypeClass (b,b') ->
+	    intern_typeclass_binder intern_type lvar (env,bl) (List.hd nal, (b,b'), ty))
   | LocalRawDef((loc,na),def) ->
       ((name_fold Idset.add na ids,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
@@ -1029,9 +1027,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
     in
       match bk with
 	| Default b -> default env b nal
-	| TypeClass b -> 
+	| TypeClass (b,b') -> 
 	    let env, ibind = intern_typeclass_binder intern_type lvar
-	      (env, []) (List.hd nal) b ty in
+	      (env, []) (List.hd nal,(b,b'),ty) in
 	    let body = intern_type env body in
 	      it_mkRProd ibind body
 					   
@@ -1045,9 +1043,9 @@ let internalise sigma globalenv env allow_patvar lvar c =
       | [] -> intern env body
     in match bk with
       | Default b -> default env b nal
-      | TypeClass b ->	  
+      | TypeClass (b, b') ->	  
 	  let env, ibind = intern_typeclass_binder intern_type lvar
-	    (env, []) (List.hd nal) b ty in
+	    (env, []) (List.hd nal,(b,b'),ty) in
 	  let body = intern env body in
 	    it_mkRLambda ibind body
 	      
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bef2573e5..d084a3f7d 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -193,6 +193,44 @@ let resolve_class_binders env l =
   in
     fv_ctx, ctx
 
+let full_class_binder env (iid, (bk, bk'), cl as c) = 
+  let avoid = Idset.union env (ids_of_list (compute_context_vars env [c])) in
+  let c, avoid =
+    match bk' with
+    | Implicit -> 
+	let (loc, id, l) = 
+	  try destClassAppExpl cl 
+	  with Not_found -> 
+	    user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
+	in
+	let gr = Nametab.global id in
+	  (try
+	      let c = class_info gr in
+	      let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
+		(iid, bk, CAppExpl (loc, (None, id), args)), avoid
+	    with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
+    | Explicit -> ((iid,bk,cl), avoid)
+  in c
+
+let compute_constraint_freevars env (oid, _, x) =
+  let bound = match snd oid with Name n -> Idset.add n env | Anonymous -> env in
+  let ids = free_vars_of_constr_expr x ~bound [] in
+    freevars_of_ids env (List.rev ids)
+
+let resolve_class_binder env c = 
+  let cstr = full_class_binder env c in
+  let fv_ctx = 
+    let elts = compute_constraint_freevars env cstr in
+      List.map (fun id -> (dummy_loc, id), CHole (dummy_loc, None)) elts
+  in fv_ctx, cstr
+    
+let generalize_class_binder_raw env c = 
+  let env = Idset.union env (Termops.vars_of_env (Global.env())) in
+  let fv_ctx, cstr = resolve_class_binder env c in
+  let ids' = List.fold_left (fun acc ((loc, id), t) -> Idset.add id acc) env fv_ctx in
+  let ctx' = List.map (fun ((loc, id), t) -> ((loc, Name id), Implicit, t)) fv_ctx in
+    ids', ctx', cstr
+
 let generalize_class_binders_raw env l = 
   let env = Idset.union env (Termops.vars_of_env (Global.env())) in
   let fv_ctx, cstrs = resolve_class_binders env l in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index bd061a1ed..ac1b8c99a 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -43,6 +43,9 @@ val resolve_class_binders : Idset.t -> typeclass_context ->
   (identifier located * constr_expr) list * typeclass_context
 
 val full_class_binders : Idset.t -> typeclass_context -> typeclass_context
+
+val generalize_class_binder_raw : Idset.t -> name located * (binding_kind * binding_kind) * constr_expr -> 
+  Idset.t * typeclass_context * typeclass_constraint
   
 val generalize_class_binders_raw : Idset.t -> typeclass_context -> 
   (name located * binding_kind * constr_expr) list * (name located * binding_kind * constr_expr) list
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cef1b9391..570eae7e5 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -590,7 +590,7 @@ type notation = string
 
 type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
 
-type binder_kind = Default of binding_kind | TypeClass of binding_kind
+type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 6790e400f..46133c27b 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -95,7 +95,7 @@ type notation = string
 
 type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
   
-type binder_kind = Default of binding_kind | TypeClass of binding_kind
+type binder_kind = Default of binding_kind | TypeClass of binding_kind * binding_kind
 
 type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
 
diff --git a/lib/util.ml b/lib/util.ml
index 14a40e378..ebade654e 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -576,6 +576,12 @@ let list_fold_left_i f =
   in 
   it_list_f 
 
+let rec list_fold_left3 f accu l1 l2 l3 =
+  match (l1, l2, l3) with
+    ([], [], []) -> accu
+  | (a1::l1, a2::l2, a3::l3) -> list_fold_left3 f (f accu a1 a2 a3) l1 l2 l3
+  | (_, _, _) -> invalid_arg "list_fold_left3"
+
 (* [list_fold_right_and_left f [a1;...;an] hd =
    f (f (... (f (f hd
                    an
diff --git a/lib/util.mli b/lib/util.mli
index 9c0756fc9..7e351e270 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -132,6 +132,7 @@ val list_fold_right_i :  (int -> 'a -> 'b -> 'b) -> int -> 'a list -> 'b -> 'b
 val list_fold_left_i :  (int -> 'a -> 'b -> 'a) -> int -> 'a -> 'b list -> 'a
 val list_fold_right_and_left :
     ('a -> 'b -> 'b list -> 'a) -> 'b list -> 'a -> 'a
+val list_fold_left3 : ('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b list -> 'c list -> 'd list -> 'a
 val list_for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool
 val list_except : 'a -> 'a list -> 'a list
 val list_remove : 'a -> 'a list -> 'a list
diff --git a/library/impargs.ml b/library/impargs.ml
index 79abdb4c9..138400953 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -88,7 +88,7 @@ let set_maximality imps b =
 
 (*s Computation of implicit arguments *)
 
-(* We remember various information about why an argument is (automatically)
+(* We remember various information about why an argument is
    inferable as implicit
 
 - [DepRigid] means that the implicit argument can be found by
@@ -105,6 +105,8 @@ let set_maximality imps b =
   inferable following a rigid path (useful to know how to print a
   partial application)
 
+- [Manual] means the argument has been explicitely set as implicit.
+
   We also consider arguments inferable from the conclusion but it is
   operational only if [conclusion_matters] is true.
 *)
@@ -117,7 +119,7 @@ type implicit_explanation =
   | DepRigid of argument_position
   | DepFlex of argument_position
   | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
-  | Manual of bool
+  | Manual
 
 let argument_less = function
   | Hyp n, Hyp n' -> n<n'
@@ -137,7 +139,7 @@ let update pos rig (na,st) =
       | Some (DepFlex fpos) ->
           if argument_less (pos,fpos) or pos=fpos then DepRigid pos
           else DepFlexAndRigid (fpos,pos)
-      | Some (Manual _) -> assert false
+      | Some Manual -> assert false
   else
     match st with
       | None -> DepFlex pos
@@ -147,7 +149,7 @@ let update pos rig (na,st) =
           if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x
       | Some (DepFlex fpos as x) ->
           if argument_less (pos,fpos) then DepFlex pos else x
-      | Some (Manual _) -> assert false
+      | Some Manual -> assert false
   in na, Some e
 
 (* modified is_rigid_reference with a truncated env *)
@@ -241,10 +243,10 @@ let compute_implicits_flags env f all t =
     f.reversible_pattern f.contextual all env t
     
 let set_implicit id imp insmax =
-  (id,(match imp with None -> Manual false | Some imp -> imp),insmax)
+  (id,(match imp with None -> Manual | Some imp -> imp),insmax)
 
 let merge_imps f = function 
-    None -> Some (Manual f)
+    None -> Some Manual
   | x -> x
 
 let rec assoc_by_pos k = function
@@ -262,7 +264,7 @@ let compute_manual_implicits env flags t enriching l =
       let (id, (b, f)), l' = assoc_by_pos k l in
 	if f then
 	  let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in
-	    l', Some (id,Manual f,b)
+	    l', Some (id,Manual,b)
 	else l, None
     with Not_found -> l, None
   in
@@ -333,10 +335,6 @@ let maximal_insertion_of = function
   | Some (_,_,b) -> b
   | None -> anomaly "Not an implicit argument"
 
-let forced_implicit = function
-  | Some (_,Manual b,_) -> b
-  | _ -> false
-
 (* [in_ctx] means we know the expected type, [n] is the index of the argument *)
 let is_inferable_implicit in_ctx n = function
   | None -> false
@@ -346,7 +344,7 @@ let is_inferable_implicit in_ctx n = function
   | Some (_,DepRigid Conclusion,_) -> in_ctx
   | Some (_,DepFlex Conclusion,_) -> false
   | Some (_,DepFlexAndRigid (_,Conclusion),_) -> in_ctx
-  | Some (_,Manual _,_) -> true
+  | Some (_,Manual,_) -> true
 
 let positions_of_implicits =
   let rec aux n = function
@@ -418,8 +416,11 @@ let list_split_at index l =
   in aux 0 [] l
     
 let merge_impls oimpls impls =
-  let oimpls, _ = list_split_at (List.length oimpls - List.length impls) oimpls in
-    oimpls @ impls
+  let oimpls, newimpls = list_split_at (List.length oimpls - List.length impls) oimpls in
+    oimpls @ (List.map2 (fun orig ni ->
+      match orig with
+      | Some (_, Manual, _) -> orig
+      | _ -> ni) impls newimpls)
 
 (* Caching implicits *)
 
@@ -545,6 +546,12 @@ let maybe_declare_manual_implicits local ref enriching l =
   if l = [] then ()
   else declare_manual_implicits local ref enriching l
 
+let lift_implicits n = 
+  List.map (fun x -> 
+    match fst x with 
+	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
+      | _ -> x)
+
 (*s Registration as global tables *)
 
 let init () = implicits_table := Refmap.empty
diff --git a/library/impargs.mli b/library/impargs.mli
index 120660027..5bfa0470d 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -47,7 +47,6 @@ val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
 val name_of_implicit : implicit_status -> identifier
 val maximal_insertion_of : implicit_status -> bool
-val forced_implicit : implicit_status -> bool
 
 val positions_of_implicits : implicits_list -> int list
 
@@ -83,3 +82,5 @@ val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
   manual_explicitation list -> unit
 
 val implicits_of_global : global_reference -> implicits_list
+
+val lift_implicits : int -> manual_explicitation list -> manual_explicitation list
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 6b6b4871c..3f437721a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -409,17 +409,19 @@ GEXTEND Gram
   ;
   typeclass_constraint_binder:
     [ [ tc = typeclass_constraint ->
-      let (n,bk,t) = tc in
-	LocalRawAssum ([n], TypeClass bk, t)
+      let (n,(b,b'),t) = tc in
+	LocalRawAssum ([n], TypeClass (b,b'), t)
     ] ]
   ;
 
   typeclass_constraint:
-    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
-    | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
-	(loc, Name iid), expl, c
-    | c = operconstr LEVEL "200" ->
-	(loc, Anonymous), Implicit, c
+    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), (Implicit, Explicit), c
+      | "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+	  id, (Implicit, expl), c
+      | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+	  (loc, Name iid), (Explicit, expl), c
+      | c = operconstr LEVEL "200" ->
+	  (loc, Anonymous), (Implicit, Implicit), c
     ] ]
   ;
   
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index aaf4324e2..19cb28778 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -166,7 +166,7 @@ module Constr :
     val binder_let : local_binder list Gram.Entry.e
     val binders_let : local_binder list Gram.Entry.e
     val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
-    val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
+    val typeclass_constraint : (name located * (binding_kind * binding_kind) * constr_expr) Gram.Entry.e
     val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
   end
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 04b700236..912406f3f 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -219,13 +219,13 @@ let surround_binder k p =
   match k with
       Default Explicit -> hov 1 (str"(" ++ p ++ str")")
     | Default Implicit -> hov 1 (str"{" ++ p ++ str"}")
-    | TypeClass b -> hov 1 (str"[" ++ p ++ str"]")
+    | TypeClass _ -> hov 1 (str"[" ++ p ++ str"]")
 
 let surround_implicit k p =
   match k with
       Default Explicit -> p
     | Default Implicit -> (str"{" ++ p ++ str"}")
-    | TypeClass b -> (str"[" ++ p ++ str"]")
+    | TypeClass _ -> (str"[" ++ p ++ str"]")
 
 let pr_binder many pr (nal,k,t) =
   match t with
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e27a93b33..6bd795ed5 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -139,7 +139,7 @@ let mlexpr_of_binding_kind = function
 
 let mlexpr_of_binder_kind = function
   | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
-  | Topconstr.TypeClass b -> <:expr< Topconstr.TypeClass $mlexpr_of_binding_kind b$ >>
+  | Topconstr.TypeClass (b,b') -> <:expr< Topconstr.TypeClass $mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_binding_kind (b,b')$ >>
 
 let rec mlexpr_of_constr = function
   | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 530fec6d1..da30b2057 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -37,8 +37,6 @@ type typeclass = {
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
   cl_context : ((global_reference * bool) option * rel_declaration) list; 
 
-  cl_params: int;
-
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : rel_context;
   
@@ -154,7 +152,7 @@ let subst (_,subst,(cl,m,inst)) =
   let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs in
   let subst_class k cl classes = 
     let k = do_subst_gr k in
-    let cl' = { cl with cl_impl = k;
+    let cl' = { cl_impl = k;
 		cl_context = do_subst_ctx cl.cl_context;
 		cl_props = do_subst_named cl.cl_props;
 		cl_projs = do_subst_projs cl.cl_projs; }
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f77be5293..60b5da822 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -32,8 +32,6 @@ type typeclass = {
      The boolean indicates if the typeclass argument is a direct superclass. *)
   cl_context : ((global_reference * bool) option * rel_declaration) list; 
 
-  cl_params : int; (* This is the length of the suffix of the context which should be considered explicit parameters. *)
-
   (* Context of definitions and properties on defs, will not be shared *)
   cl_props : rel_context;
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 3ffa8040d..2c1a7deb9 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -321,11 +321,11 @@ Class MorphismProxy A (R : relation A) (m : A) : Prop :=
   respect_proxy : R m m.
 
 Instance reflexive_morphism_proxy
-  [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1.
+  [ Reflexive A R ] (x : A) : MorphismProxy R x | 1.
 Proof. firstorder. Qed.
 
 Instance morphism_morphism_proxy
-  [ Morphism A R x ] : MorphismProxy A R x | 2.
+  [ Morphism A R x ] : MorphismProxy R x | 2.
 Proof. firstorder. Qed.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
@@ -376,17 +376,17 @@ Class (A : Type) => Normalizes (m : relation A) (m' : relation A) : Prop :=
   normalizes : relation_equivalence m m'.
 
 Instance inverse_respectful_norm : 
-  Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
+  ! Normalizes (A -> B) (inverse R ==> inverse R') (inverse (R ==> R')) .
 Proof. firstorder. Qed.
 
 (* If not an inverse on the left, do a double inverse. *)
 
 Instance not_inverse_respectful_norm : 
-  Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
+  ! Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4.
 Proof. firstorder. Qed.
 
 Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] :
-  Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
+  ! Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')).
 Proof. red ; intros. 
   assert(r:=normalizes).
   setoid_rewrite r.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index c4e98c24a..99eda0ae1 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -43,7 +43,7 @@ Class Reflexive A (R : relation A) :=
   reflexivity : forall x, R x x.
 
 Class Irreflexive A (R : relation A) := 
-  irreflexivity :> Reflexive A (complement R).
+  irreflexivity :> Reflexive (complement R).
 
 Class Symmetric A (R : relation A) := 
   symmetry : forall x y, R x y -> R y x.
@@ -54,12 +54,6 @@ Class Asymmetric A (R : relation A) :=
 Class Transitive A (R : relation A) := 
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
-Implicit Arguments Reflexive [A].
-Implicit Arguments Irreflexive [A].
-Implicit Arguments Symmetric [A].
-Implicit Arguments Asymmetric [A].
-Implicit Arguments Transitive [A].
-
 Hint Resolve @irreflexivity : ord.
 
 Unset Implicit Arguments.
@@ -178,7 +172,7 @@ Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 :=
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
-Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
+Class [ equ : Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
 Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] :
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 4d6601a6e..07a6985c9 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -27,12 +27,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class [ Setoid A ] => DecidableSetoid :=
+Class DecidableSetoid A [ Setoid A ] :=
   setoid_decidable : forall x y : A, decidable (x == y).
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class [ Setoid A ] => EqDec :=
+Class [ s : Setoid A ] => EqDec :=
   equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
@@ -75,18 +75,18 @@ Require Import Coq.Arith.Arith.
 
 (** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
 
-Program Instance eq_setoid : Setoid A :=
+Program Instance eq_setoid A : Setoid A :=
   equiv := eq ; setoid_equiv := eq_equivalence.
 
-Program Instance nat_eq_eqdec : EqDec (@eq_setoid nat) :=
+Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
   equiv_dec := eq_nat_dec.
 
 Require Import Coq.Bool.Bool.
 
-Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
+Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
   equiv_dec := bool_dec.
 
-Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
+Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
   equiv_dec x y := in_left.
 
   Next Obligation.
@@ -95,7 +95,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) :=
+Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : EqDec (eq_setoid (prod A B)) :=
   equiv_dec x y := 
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
@@ -110,7 +110,7 @@ Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] :
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) :=
+Program Instance bool_function_eqdec [ ! EqDec (eq_setoid A) ] : EqDec (eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then in_left
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index ff5f7cb6c..e939d3ee7 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -38,7 +38,7 @@ Definition default_relation [ DefaultRelation A R ] := R.
 
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
-Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4.
+Instance equivalence_default [ Equivalence A R ] : DefaultRelation R | 4.
 
 (** The setoid_replace tactics in Ltac, defined in terms of default relations and
    the setoid_rewrite tactic. *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index d07051b71..5599f4d66 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -110,40 +110,15 @@ let interp_fields_evars isevars env avoid l =
 
 open Topconstr
 
-let declare_implicit_proj c proj imps sub =
-  let len = List.length c.cl_context in
-  let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) (snd proj)) in
-  let expls =
-    let rec aux i expls = function
-	[] -> expls
-      | (Name n, _) :: tl -> 
-	  let impl = ExplByPos (i, Some n), (true, true) in
-	    aux (succ i) (impl :: List.remove_assoc (ExplByName n) expls) tl
-      | (Anonymous,_) :: _ -> assert(false)
-    in
-      aux 1 [] (List.rev ctx)
-  in 
-  let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in
-    if sub then 
-      declare_instance_cst true (snd proj);
-    Impargs.declare_manual_implicits false (ConstRef (snd proj)) true expls
-      
-let declare_implicits impls subs cl =
-  Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub)
-    cl.cl_projs impls subs;
-  let len = List.length cl.cl_context in
-  let indimps = 
-    list_fold_left_i 
-      (fun i acc (is, (na, b, t)) -> 
-	if len - i <= cl.cl_params then acc
-	else 
-	  match is with
-	      None | Some (_, false) -> (ExplByPos (i, Some (Nameops.out_name na)), (false, true)) :: acc
-	    | _ -> acc)
-      1 [] (List.rev cl.cl_context)
-  in
-    Impargs.declare_manual_implicits false cl.cl_impl false indimps
-      
+let implicits_of_context ctx =
+  list_map_i (fun i name ->
+    let explname = 
+      match name with 
+      | Name n -> Some n
+      | Anonymous -> None
+    in ExplByPos (i, explname), (true, true))
+    1 (List.rev (Anonymous :: (List.map pi1 ctx)))
+
 let degenerate_decl (na,b,t) =
   let id = match na with
     | Name id -> id
@@ -152,29 +127,6 @@ let degenerate_decl (na,b,t) =
     | None -> (id, Entries.LocalAssum t)
     | Some b -> (id, Entries.LocalDef b)
 
-let declare_structure env id idbuild params arity fields =
-  let nparams = List.length params and nfields = List.length fields in
-  let args = extended_rel_list nfields params in
-  let ind = applist (mkRel (1+nparams+nfields), args) in
-  let type_constructor = it_mkProd_or_LetIn ind fields in
-  let mie_ind =
-    { mind_entry_typename = id;
-      mind_entry_arity = arity;
-      mind_entry_consnames = [idbuild];
-      mind_entry_lc = [type_constructor] } in
-  let mie =
-    { mind_entry_params = List.map degenerate_decl params;
-      mind_entry_record = true;
-      mind_entry_finite = true;
-      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 id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
-  let kinds,sp_projs = Record.declare_projections rsp ~kind:Method ~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
-
 let name_typeclass_binder avoid = function
   | LocalRawAssum ([loc, Anonymous], bk, c) ->
       let name = 
@@ -235,6 +187,12 @@ let new_class id par ar sup props =
   let ctx_props = Evarutil.nf_rel_context_evar sigma ctx_props in
   let arity = Reductionops.nf_evar sigma arity in
   let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
+  let fieldimpls = 
+    (* Make the class and all params implicits in the projections *)
+    let ctx_impls = implicits_of_context ctx_params in
+    let len = succ (List.length ctx_params) in
+      List.rev_map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls
+  in
   let impl, projs = 
     let params = ctx_params and fields = ctx_props in
       List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
@@ -267,12 +225,18 @@ let new_class id par ar sup props =
 	    let proj_cst = Declare.declare_constant proj_name
 	      (DefinitionEntry proj_entry, IsDefinition Definition) 
 	    in
-	      ConstRef cst, [proj_name, proj_cst]
+	    let cref = ConstRef cst in
+	      Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps;
+	      Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls);
+	      cref, [proj_name, proj_cst]
 	| _ ->
 	    let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
-	    let kn = declare_structure env0 (snd id) idb params arity fields in
-	      IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
-			     fields (Recordops.lookup_projections kn))
+	    let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
+	    let kn = Record.declare_structure (snd id) idb arity_imps
+	      params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
+	    in
+	      IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
+			     fields (Recordops.lookup_projections (kn,0)))
   in
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
@@ -283,12 +247,12 @@ let new_class id par ar sup props =
   in
   let k =
     { cl_impl = impl;
-      cl_params = List.length par;
       cl_context = ctx_context;
       cl_props = ctx_props;
       cl_projs = projs }
   in
-    declare_implicits (List.rev prop_impls) subs k;
+    List.iter2 (fun p sub -> if sub then declare_instance_cst true (snd p))
+      k.cl_projs subs;
     add_class k
     
 type binder_def_list = (identifier located * identifier located list * constr_expr) list
@@ -489,12 +453,17 @@ let context ?(hook=fun _ -> ()) l =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let avoid = Termops.ids_of_context env in
-  let ctx, l = Implicit_quantifiers.resolve_class_binders (vars_of_env env) l in
-  let env', avoid, ctx = interp_binders_evars isevars env avoid ctx in
-  let env', avoid, l = interp_typeclass_context_evars isevars env' avoid l in
+  let ctx, l = 
+    List.fold_left 
+      (fun (ids, acc) x ->
+	let ids, ctx, cstr = Implicit_quantifiers.generalize_class_binder_raw ids x in
+	  (ids, (cstr :: ctx) @ acc))
+      (vars_of_env env, []) l
+  in
+  let env', avoid, l = interp_typeclass_context_evars isevars env avoid (List.rev l) in
   isevars := Evarutil.nf_evar_defs !isevars;
   let sigma = Evd.evars_of !isevars in
-  let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in
+  let fullctx = Evarutil.nf_named_context_evar sigma l in
     List.iter (function (id,_,t) -> 
       if Lib.is_modtype () then 
 	let cst = Declare.declare_internal_constant id
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 3bc5d0326..c10ee4c97 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -38,8 +38,8 @@ val name_typeclass_binders : Idset.t ->
     Topconstr.local_binder list ->
     Topconstr.local_binder list * Idset.t
 
-val declare_implicit_proj : typeclass -> (identifier * constant) -> 
-  Impargs.manual_explicitation list -> bool -> unit
+(* val declare_implicit_proj : typeclass -> (identifier * constant) ->  *)
+(*   Impargs.manual_explicitation list -> bool -> unit *)
 
 val new_class : identifier located ->
   local_binder list ->
@@ -85,7 +85,9 @@ val id_of_class : typeclass -> identifier
 
 (* Context command *)    
 
-val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit
+val context : ?hook:(Libnames.global_reference -> unit) -> 
+  (Names.name Util.located * (Rawterm.binding_kind * Rawterm.binding_kind) *
+  Topconstr.constr_expr) list -> unit
 
 (* Forward ref for refine *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index df133e769..14e64ead4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -613,13 +613,6 @@ let _ =
       optread  = (fun () -> !elim_flag) ;
       optwrite = (fun b -> elim_flag := b) }
 
-
-let lift_implicits n = 
-  List.map (fun x -> 
-    match fst x with 
-	ExplByPos (k, id) -> ExplByPos (k + n, id), snd x
-      | _ -> x)
-
 let declare_mutual_with_eliminations isrecord mie impls =
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let params = List.length mie.mind_entry_params in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 83332e823..ab06673e4 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -31,29 +31,41 @@ open Topconstr
 
 (********** definition d'un record (structure) **************)
 
-let interp_decl sigma env = function
-  | Vernacexpr.AssumExpr((_,id),t) -> (id,None,interp_type Evd.empty env t)
-  | Vernacexpr.DefExpr((_,id),c,t) ->
-      let c = match t with
-	| None -> c
-	| Some t -> mkCastC (c, Rawterm.CastConv (DEFAULTcast,t))
-      in
-      let j = interp_constr_judgment Evd.empty env c in
-      (id,Some j.uj_val, refresh_universes j.uj_type)
+let interp_evars evdref env ?(impls=([],[])) k typ =
+  let typ' = intern_gen true ~impls (Evd.evars_of !evdref) env typ in
+  let imps = Implicit_quantifiers.implicits_of_rawterm typ' in
+    imps, Pretyping.Default.understand_tcc_evars evdref env k typ'
+
+let mk_interning_data env na impls typ =
+  let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
+  in (out_name na, ([], impl, Notation.compute_arguments_scope typ))
+    
+let interp_fields_evars isevars env l =
+  List.fold_left
+    (fun (env, uimpls, params, impls) ((loc, i), b, t) ->
+      let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in
+      let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in
+      let data = mk_interning_data env i impl t' in
+      let d = (i,b',t') in
+	(push_rel d env, impl :: uimpls, d::params, ([], data :: snd impls)))
+    (env, [], [], ([], [])) l    
+
+let binder_of_decl = function
+  | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
+  | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c | None -> CHole (fst n, None))
+
+let binders_of_decls = List.map binder_of_decl
 
 let typecheck_params_and_fields id t ps fs =
   let env0 = Global.env () in
-  let (env1,newps), _ = interp_context Evd.empty env0 ps in
+  let (env1,newps), imps = interp_context Evd.empty env0 ps in
   let fullarity = it_mkProd_or_LetIn t newps in
   let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
-  let env2,newfs =
-    List.fold_left
-      (fun (env,newfs) d ->
-         let decl = interp_decl Evd.empty env d in
-         (push_rel decl env, decl::newfs))
-      (env_ar,[]) fs
+  let evars = ref (Evd.create_evar_defs Evd.empty) in
+  let env2,impls,newfs,data =
+    interp_fields_evars evars env_ar (binders_of_decls fs)
   in
-  newps, newfs
+    imps, newps, impls, newfs
 
 let degenerate_decl (na,b,t) =
   let id = match na with
@@ -131,7 +143,7 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
   substl_rel_context (subst@[mkInd indsp]) fields
 
 (* We build projections *)
-let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
+let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let paramdecls = mib.mind_params_ctxt in
@@ -142,8 +154,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
   let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
   let lifted_fields = lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
-    List.fold_left2
-      (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) ->
+    list_fold_left3
+      (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) impls ->
 	let (sp_projs,subst) =
 	  match fi with
 	  | Anonymous ->
@@ -180,6 +192,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
 	      let refi = ConstRef kn in
 	      let constr_fi = mkConst kn in
+	      Impargs.maybe_declare_manual_implicits 
+		false refi (Impargs.is_implicit_args()) impls;
 	      if coe then begin
 	        let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi Global cl
@@ -191,28 +205,18 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,NoProjection fi::subst) in
       (nfi-1,(optci=None)::kinds,sp_projs,subst))
-      (List.length fields,[],[],[]) coers (List.rev fields)
+      (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
-(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
-   list telling if the corresponding fields must me declared as coercion *)
-let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
-  let coers,fs = List.split cfs in
-  let extract_name acc = function
-      Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
-    | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
-    | _ -> acc in
-  let allnames =  idstruc::(List.fold_left extract_name [] fs) in
-  if not (list_distinct allnames) then error "Two objects have the same name";
-  (* Now, younger decl in params and fields is on top *)
-  let params,fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
+let declare_structure id idbuild paramimpls params arity fieldimpls fields
+    ?(kind=StructureComponent) ?name is_coe coers =
   let nparams = List.length params and nfields = List.length fields in
   let args = extended_rel_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let mie_ind =
-    { mind_entry_typename = idstruc;
-      mind_entry_arity = mkSort s;
+    { mind_entry_typename = id;
+      mind_entry_arity = arity;
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] } in
   let declare_as_coind =
@@ -223,10 +227,27 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
       mind_entry_record = true;
       mind_entry_finite = not declare_as_coind;
       mind_entry_inds = [mie_ind] } in
-  let kn = declare_mutual_with_eliminations true mie [] in
+  let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
-  let kinds,sp_projs = declare_projections rsp coers fields in
-  let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
-  if is_coe then Class.try_add_new_coercion build Global;
-  Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
-  kn
+  let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
+  let build = ConstructRef (rsp,1) in
+    if is_coe then Class.try_add_new_coercion build Global;
+    Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
+    kn
+
+(* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
+   list telling if the corresponding fields must me declared as coercion *)
+let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
+  let coers,fs = List.split cfs in
+  let extract_name acc = function
+      Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
+    | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
+    | _ -> acc in
+  let allnames =  idstruc::(List.fold_left extract_name [] fs) in
+  if not (list_distinct allnames) then error "Two objects have the same name";
+  (* Now, younger decl in params and fields is on top *)
+  let implpars, params, implfs, fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
+  let implfs = List.map 
+    (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
+    declare_structure idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers
+  
diff --git a/toplevel/record.mli b/toplevel/record.mli
index c2c6b72ee..7799162df 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -14,6 +14,7 @@ open Term
 open Sign
 open Vernacexpr
 open Topconstr
+open Impargs
 (*i*)
 
 (* [declare_projections ref name coers params fields] declare projections of
@@ -21,7 +22,18 @@ open Topconstr
    as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
+  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+  bool list -> manual_explicitation list list -> rel_context -> 
+  bool list * constant option list
+
+val declare_structure : identifier -> identifier -> 
+  manual_explicitation list -> rel_context -> (* params *)
+  Term.constr -> (* arity *)
+  Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *)
+  ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+  bool -> (* coercion? *)
+  bool list -> (* field coercions *)
+  mutual_inductive
 
 val definition_structure :
   lident with_coercion * local_binder list *
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8f54e699e..2c646f6bc 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -239,7 +239,9 @@ type vernac_expr =
 	(lident * lident list * constr_expr) list * (* props *)
 	int option (* Priority *)
 
-  | VernacContext of typeclass_context
+  | VernacContext of 
+      (Names.name Util.located * (Rawterm.binding_kind * Rawterm.binding_kind) *
+	  Topconstr.constr_expr) list
 	
   | VernacDeclareInstance of
       lident (* instance name *)