Fix a bug found by B. Grégoire when declaring morphisms in module

types. Change (again) the semantics of bindings and the binding modifier
! in typeclasses. Inside [ ], implicit binding where only parameters
need to be given is the default, use ! to use explicit binding, which is
equivalent to regular bindings except for generalization of free
variables. Outside brackets (e.g. on the right of instance
declarations),  explicit binding is the default, and implicit binding
can be used by adding ! in front. This avoids almost every use of ! in
the standard library and in other examples I have.


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

13 files changed, 168 insertions, 150 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 39865f1f9..0c99fe16e 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -107,7 +107,7 @@ let new_instance ctx (instid, bk, cl) props pri =
   let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
   let tclass =
     match bk with
-      | Explicit ->
+      | Implicit ->
 	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
 	  let k = class_info (Nametab.global id) in
 	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
@@ -128,7 +128,7 @@ let new_instance ctx (instid, bk, cl) props pri =
 	      par (List.rev k.cl_context)
 	    in Topconstr.CAppExpl (loc, (None, id), pars)
 
-      | Implicit -> cl
+      | Explicit -> cl
   in
   let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
   let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3b2b5d3d4..3551746b8 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -172,7 +172,7 @@ let full_class_binders env l =
   let l', avoid =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
-	  Explicit -> 
+	  Implicit -> 
 	    let (loc, id, l) = destClassAppExpl cl in
 	    let gr = Nametab.global id in
 	      (try
@@ -180,14 +180,14 @@ let full_class_binders env l =
 		  let args, avoid = combine_params_freevar avoid l (List.rev c.cl_context) in
 		    (iid, bk, CAppExpl (loc, (None, id), args)) :: l', avoid
 		with Not_found -> not_a_class (Global.env ()) (constr_of_global gr))
-	| Implicit -> (x :: l', avoid))
+	| Explicit -> (x :: l', avoid))
       ([], avoid) l
   in List.rev l'
       
 let constr_expr_of_constraint (kind, id) l =
   match kind with
-    | Explicit -> CAppExpl (fst id, (None, Ident id), l)
-    | Implicit -> CApp (fst id, (None, CRef (Ident id)),
+    | Implicit -> CAppExpl (fst id, (None, Ident id), l)
+    | Explicit -> CApp (fst id, (None, CRef (Ident id)),
 		       List.map (fun x -> x, None) l)
 
 (*    | CApp of loc * (proj_flag * constr_expr) *  *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3b6740731..40c6180f0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -492,6 +492,11 @@ GEXTEND Gram
       | IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
 	 is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
 	   let sup = match sup with None -> [] | Some l -> l in
+	   let is = (* We reverse the default binding mode on the right *)
+	     let n, bk, t = is in
+	       n, (match bk with Rawterm.Implicit -> Rawterm.Explicit 
+		 | Rawterm.Explicit -> Rawterm.Implicit), t 
+	   in
 	     VernacInstance (sup, is, props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a3baa1abb..4f740f865 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -973,11 +973,11 @@ END
     
 let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
 
-let declare_instance a aeq n s = ((dummy_loc,Name n),Explicit,
-				  CApp (dummy_loc, (None, mkRefC (Qualid (dummy_loc, qualid_of_string s))), 
-					[(a,None);(aeq,None)]))
+let declare_instance a aeq n s = ((dummy_loc,Name n), Explicit,
+				 CAppExpl (dummy_loc, (None, Qualid (dummy_loc, qualid_of_string s)), 
+					  [a;aeq]))
 
-let anew_instance instance fields = new_instance [] instance fields None (fun _ -> ())
+let anew_instance instance fields = new_instance [] instance fields None
 
 let require_library dirpath =
   let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
@@ -1104,6 +1104,7 @@ let declare_projection n instance_id r =
   let c = constr_of_global r in
   let term = respect_projection c ty in
   let typ = Typing.type_of (Global.env ()) Evd.empty term in
+  let ctx, typ = Sign.decompose_prod_assum typ in
   let typ =
     let n = 
       let rec aux t = 
@@ -1122,6 +1123,7 @@ let declare_projection n instance_id r =
     let ctx,ccl = Reductionops.decomp_n_prod (Global.env()) Evd.empty (3 * n) typ
     in it_mkProd_or_LetIn ccl ctx 
   in
+  let typ = it_mkProd_or_LetIn typ ctx in
   let cst = 
     { const_entry_body = term;
       const_entry_type = Some typ;
@@ -1209,18 +1211,15 @@ VERNAC COMMAND EXTEND AddSetoid1
       [ init_setoid ();
 	let instance_id = add_suffix n "_Morphism" in
 	let instance = 
-	  ((dummy_loc,Name instance_id), Implicit,
-	  CApp (dummy_loc, (None, mkRefC 
-	    (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism"))), 
-	       [(s,None);(m,None)]))
-	in
-	  if Lib.is_modtype () then (context ~hook:(fun r -> declare_projection n instance_id r) [ instance ])
-	  else (
-	    Flags.silently 
-	      (fun () ->
-		ignore(new_instance [] instance [] None (fun cst -> declare_projection n instance_id (ConstRef cst)));
-		Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();
-	    Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) ())
+	  ((dummy_loc,Name instance_id), Explicit,
+	  CAppExpl (dummy_loc, 
+		   (None, Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Classes.Morphisms.Morphism")), 
+		   [cHole; s; m]))
+	in	  
+	let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
+	  ignore(new_instance [] instance []
+		    ~tac ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst))
+		    None)
       ]
 END
 
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 58aef9a7b..d0c999196 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -30,23 +30,23 @@ Open Local Scope signature_scope.
 
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
-Instance [ ! Equivalence A R ] => 
+Instance [ Equivalence A R ] => 
   equivalence_default : DefaultRelation A R | 4.
 
 Definition equiv [ Equivalence A R ] : relation A := R.
 
 (** Shortcuts to make proof search possible (unification won't unfold equiv). *)
 
-Program Instance [ sa : ! Equivalence A ] => equiv_refl : Reflexive equiv.
+Program Instance [ sa : Equivalence A ] => equiv_refl : Reflexive equiv.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_sym : Symmetric equiv.
+Program Instance [ sa : Equivalence A ] => equiv_sym : Symmetric equiv.
 
   Next Obligation.
   Proof.
     symmetry ; auto.
   Qed.
 
-Program Instance [ sa : ! Equivalence A ] => equiv_trans : Transitive equiv.
+Program Instance [ sa : Equivalence A ] => equiv_trans : Transitive equiv.
 
   Next Obligation.
   Proof.
@@ -81,7 +81,7 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
+Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
   intros; intro.
   assert(z === y) by (symmetry ; auto).
@@ -89,7 +89,7 @@ Proof with auto.
   contradiction.
 Qed.
 
-Lemma equiv_nequiv_trans : forall [ ! Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
+Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
   assert(y === x) by (symmetry ; auto).
@@ -116,12 +116,12 @@ Ltac equivify := repeat equivify_tac.
 
 (** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *)
 
-Instance [ sa : ! Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
+Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv :=
   respect := respect.
 
 (** The partial application too as it is Reflexive. *)
 
-Instance [ sa : ! Equivalence A ] (x : A) => 
+Instance [ sa : Equivalence A ] (x : A) => 
   equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) :=
   respect := respect. 
 
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 28fa55ee1..4750df639 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
   injective : forall x y : A, RB (f x) (f y) -> RA x y.
 
-Class [ m : ! Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
+Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
   surjective : forall y, exists x : A, RB y (f x).
 
-Definition Bijective [ m : ! Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
   Injective m /\ Surjective m.
 
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
   monic :> Injective m.
 
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
   epic :> Surjective m.
 
-Class [ m : ! Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
   monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
 
-Class [ m : ! Morphism (A -> A) (eqA ++> eqA), IsoMorphism m ] => AutoMorphism.
+Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index f4ec50989..eda2aecaa 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -152,7 +152,7 @@ Proof.
   reduce. apply* H.  apply* sub. assumption.
 Qed.
 
-Lemma subrelation_morphism [ SubRelation A R₁ R₂, Morphism R₂ m ] : Morphism R₁ m.
+Lemma subrelation_morphism [ SubRelation A R₁ R₂, ! Morphism R₂ m ] : Morphism R₁ m.
 Proof.
   intros. apply* H. apply H0.
 Qed.
@@ -177,7 +177,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl
 
 (* Typeclasses eauto := debug. *)
 
-Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
+Program Instance [ Symmetric A R, Morphism _ (R ==> impl) m ] => Reflexive_impl_iff : Morphism (R ==> iff) m.
 
   Next Obligation.
   Proof.
@@ -186,7 +186,7 @@ Program Instance [ ! Symmetric A R, Morphism (R ==> impl) m ] => Reflexive_impl_
 
 (** The complement of a relation conserves its morphisms. *)
 
-Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] => 
+Program Instance [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] => 
   complement_morphism : Morphism (RA ==> RA ==> iff) (complement R).
 
   Next Obligation.
@@ -200,7 +200,7 @@ Program Instance {A} (RA : relation A) [ mR : Morphism (RA ==> RA ==> iff) R ] =
 
 (** The inverse too. *)
 
-Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] => 
+Program Instance [ Morphism (A -> _) (RA ==> RA ==> iff) R ] => 
   inverse_morphism : Morphism (RA ==> RA ==> iff) (inverse R).
 
   Next Obligation.
@@ -208,7 +208,7 @@ Program Instance {A} (RA : relation A) [ Morphism (RA ==> RA ==> iff) R ] =>
     apply respect ; auto.
   Qed.
 
-Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C) ] => 
+Program Instance [ Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => 
   flip_morphism : Morphism (RB ==> RA ==> RC) (flip f).
 
   Next Obligation.
@@ -219,7 +219,7 @@ Program Instance {A B C : Type} [ Morphism (RA ==> RB ==> RC) (f : A -> B -> C)
 (** Every Transitive relation gives rise to a binary morphism on [impl], 
    contravariant in the first argument, covariant in the second. *)
 
-Program Instance [ ! Transitive A (R : relation A) ] => 
+Program Instance [ Transitive A R ] => 
   trans_contra_co_morphism : Morphism (R --> R ++> impl) R.
 
   Next Obligation.
@@ -230,7 +230,7 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
 (** Dually... *)
 
-Program Instance [ ! Transitive A (R : relation A) ] =>
+Program Instance [ Transitive A R ] =>
   trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R.
   
   Next Obligation.
@@ -252,7 +252,7 @@ Program Instance [ ! Transitive A (R : relation A) ] =>
 
 (** Morphism declarations for partial applications. *)
 
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
   trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x).
 
   Next Obligation.
@@ -260,7 +260,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ ! Transitive A R ] (x : A) =>
+Program Instance [ Transitive A R ] (x : A) =>
   trans_co_impl_morphism : Morphism (R ==> impl) (R x).
 
   Next Obligation.
@@ -268,7 +268,7 @@ Program Instance [ ! Transitive A R ] (x : A) =>
     transitivity x0...
   Qed.
 
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric A R ] (x : A) =>
   trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x).
 
   Next Obligation.
@@ -276,7 +276,7 @@ Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
     transitivity y...
   Qed.
 
-Program Instance [ ! Transitive A R, Symmetric R ] (x : A) =>
+Program Instance [ Transitive A R, Symmetric _ R ] (x : A) =>
   trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x).
 
   Next Obligation.
@@ -309,14 +309,13 @@ Program Instance [ Equivalence A R ] (x : A) =>
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Program Instance (A B : Type) (R : relation A) (R' : relation B)
-  [ Morphism (R ==> R') m ] [ Reflexive R ] (x : A) =>
+Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive _ R ] (x : A) =>
   Reflexive_partial_app_morphism : Morphism R' (m x) | 3.
 
 (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
    to get an [R y z] goal. *)
 
-Program Instance [ ! Transitive A R ] => 
+Program Instance [ Transitive A R ] => 
   trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R.
 
   Next Obligation.
@@ -324,7 +323,7 @@ Program Instance [ ! Transitive A R ] =>
     transitivity y...
   Qed.
 
-Program Instance [ ! Transitive A R ] => 
+Program Instance [ Transitive A R ] => 
   trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R.
 
   Next Obligation.
@@ -334,7 +333,7 @@ Program Instance [ ! Transitive A R ] =>
 
 (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *)
 
-Program Instance [ ! Transitive A R, Symmetric R ] => 
+Program Instance [ Transitive A R, Symmetric _ R ] => 
   trans_sym_morphism : Morphism (R ==> R ==> iff) R.
 
   Next Obligation.
@@ -421,11 +420,11 @@ Program Instance or_iff_morphism :
 (*   red ; intros. subst ; split; trivial. *)
 (* Qed. *)
 
-Instance (A B : Type) [ ! Reflexive B R ] (m : A -> B) =>
-  eq_Reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
+Instance (A : Type) [ Reflexive B R ] (m : A -> B) =>
+  eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3.
 Proof. simpl_relation. Qed.
 
-Instance (A B : Type) [ ! Reflexive B R' ] => 
+Instance (A : Type) [ Reflexive B R' ] => 
   Reflexive (@Logic.eq A ==> R').
 Proof. simpl_relation. Qed.
 
@@ -469,9 +468,8 @@ Proof.
   symmetry ; apply inverse_respectful.
 Qed.
 
-Instance (A : Type) (R : relation A) (B : Type) (R' R'' : relation B) 
-  [ Normalizes relation_equivalence R' (inverse R'') ] =>
-  Normalizes relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
+Instance [ Normalizes (relation B) relation_equivalence R' (inverse R'') ] =>
+  ! Normalizes (relation (A -> B)) relation_equivalence (inverse R ==> R') (inverse (R ==> R'')) .
 Proof.
   red.
   pose normalizes.
@@ -480,9 +478,8 @@ Proof.
   reflexivity.
 Qed.
 
-Program Instance (A : Type) (R : relation A)
-  [ Morphism R m ] => morphism_inverse_morphism :
-  Morphism (inverse R) m | 2.
+Program Instance [ Morphism A R m ] => 
+  morphism_inverse_morphism : Morphism (inverse R) m | 2.
 
 (** Bootstrap !!! *)
 
@@ -497,9 +494,9 @@ Proof.
   apply respect.
 Qed.
   
-Lemma morphism_releq_morphism (A : Type) (R : relation A) (R' : relation A)
-  [ Normalizes relation_equivalence R R' ]
-  [ Morphism R' m ] : Morphism R m.
+Lemma morphism_releq_morphism 
+  [ Normalizes (relation A) relation_equivalence R R',
+    Morphism _ R' m ] : Morphism R m.
 Proof.
   intros.
   pose respect.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 492b8498a..0ca074589 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -75,48 +75,48 @@ Hint Resolve @irreflexivity : ord.
 
 (** We can already dualize all these properties. *)
 
-Program Instance [ ! Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
+Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
+Program Instance [ Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
+Program Instance [ Symmetric A R ] => flip_Symmetric : Symmetric (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric.
 
-Program Instance [ ! Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
+Program Instance [ Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R).
   
   Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! Transitive A R ] => flip_Transitive : Transitive (flip R).
+Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
 
 (** Have to do it again for Prop. *)
 
-Program Instance [ ! Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
+Program Instance [ Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
   reflexivity := reflexivity (R:=R).
 
-Program Instance [ ! Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
+Program Instance [ Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
   irreflexivity := irreflexivity (R:=R).
 
-Program Instance [ ! Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
+Program Instance [ Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply Symmetric.
 
-Program Instance [ ! Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
+Program Instance [ Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
   
   Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry.
 
-Program Instance [ ! Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
+Program Instance [ Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
 
   Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity.
 
-Program Instance [ ! Reflexive A (R : relation A) ] => 
+Program Instance [ Reflexive A (R : relation A) ] => 
   Reflexive_complement_Irreflexive : Irreflexive (complement R).
 
-Program Instance [ ! Irreflexive A (R : relation A) ] => 
+Program Instance [ Irreflexive A (R : relation A) ] => 
   Irreflexive_complement_Reflexive : Reflexive (complement R).
 
   Next Obligation. 
@@ -125,7 +125,7 @@ Program Instance [ ! Irreflexive A (R : relation A) ] =>
     apply (irreflexivity H).
   Qed.
 
-Program Instance [ ! Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
+Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R).
 
   Next Obligation.
   Proof.
@@ -210,10 +210,10 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) :=
 Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := 
   antisymmetry : forall x y, R x y -> R y x -> eqA x y.
 
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq R ] => 
+Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq R ] => 
   flip_antiSymmetric : Antisymmetric eq (flip R).
 
-Program Instance [ eq : Equivalence A eqA, Antisymmetric eq (R : relation A) ] => 
+Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq (R : relation A) ] => 
   inverse_antiSymmetric : Antisymmetric eq (inverse R).
 
 (** Leibinz equality [eq] is an equivalence relation. *)
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 86a2bef80..26e1ab244 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -54,7 +54,7 @@ Open Local Scope program_scope.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
@@ -62,10 +62,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ ! EqDec A ] (x y : A) : bool :=
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
   if x == y then true else false.
 
-Definition nequiv_decb [ ! EqDec A ] (x y : A) : bool :=
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
   negb (equiv_decb x y).
 
 Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -97,7 +97,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => 
+Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => 
   prod_eqdec : EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
     dest x as (x1, x2) in 
@@ -113,7 +113,7 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] =>
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
+Program Instance [ ! EqDec (@eq_setoid A) ] => bool_function_eqdec : 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/toplevel/classes.ml b/toplevel/classes.ml
index cff8bce1e..9a0a0981e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -401,14 +401,14 @@ open Pp
 
 let ($$) g f = fun x -> g (f x)
 
-let new_instance ctx (instid, bk, cl) props pri hook =
+let new_instance ctx (instid, bk, cl) props ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
   let bound, fvs = Implicit_quantifiers.free_vars_of_binders ~bound [] ctx in
   let tclass = 
     match bk with
-      | Explicit ->
+      | Implicit ->
 	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
 	  let k = class_info (global id) in
 	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
@@ -429,7 +429,7 @@ let new_instance ctx (instid, bk, cl) props pri hook =
 	      par (List.rev k.cl_context)
 	    in Topconstr.CAppExpl (loc, (None, id), pars)
 
-      | Implicit -> cl
+      | Explicit -> cl
   in
   let ctx_bound = Idset.union bound (Implicit_quantifiers.ids_of_list fvs) in
   let gen_ids = Implicit_quantifiers.free_vars_of_constr_expr ~bound:ctx_bound tclass [] in
@@ -461,34 +461,7 @@ let new_instance ctx (instid, bk, cl) props pri hook =
   isevars := resolve_typeclasses env sigma !isevars;
   let sigma = Evd.evars_of !isevars in
   let substctx = Typeclasses.nf_substitution sigma subst in
-  let subst, _propsctx = 
-    let props = 
-      List.map (fun (x, l, d) -> 
-	x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
-	props
-    in
-      if List.length props > List.length k.cl_props then 
-	mismatched_props env' (List.map snd props) k.cl_props;
-      let props, rest = 
-	List.fold_left
-	  (fun (props, rest) (id,_,_) -> 
-	    try 
-	      let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
-	      let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
-		c :: props, rest'
-	    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))
-	else
-	  type_ctx_instance isevars env' k.cl_props props substctx
-  in
   let inst_constr, ty_constr = instance_constructor k in
-  let app = inst_constr (List.rev_map snd subst) in 
-  let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
-  isevars := Evarutil.nf_evar_defs !isevars;
-  let term = Evarutil.nf_isevar !isevars term in
   let termtype = 
     let app = applistc ty_constr (List.rev_map snd substctx) in
     let t = it_mkNamedProd_or_LetIn app ctx' in
@@ -499,40 +472,82 @@ let new_instance ctx (instid, bk, cl) props pri hook =
       (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
       1 ctx'
   in
-  let hook cst = 
-    let inst = 
-      { is_class = k;
-	is_pri = pri;
-	is_impl = cst;
-      }
-    in
-      Impargs.declare_manual_implicits false (ConstRef cst) false imps;
-      Typeclasses.add_instance inst;
-      hook cst
-  in
-  let evm = Evd.evars_of (undefined_evars !isevars) in
-    if evm = Evd.empty then
-      let cdecl = 
-	let kind = IsDefinition Instance in
-	let entry = 
-	  { const_entry_body   = term;
-	    const_entry_type   = Some termtype;
-	    const_entry_opaque = false;
-	    const_entry_boxed  = false }
-	in DefinitionEntry entry, kind
-      in
-      let kn = Declare.declare_constant id cdecl in
-	Flags.if_verbose Command.definition_message id;
-	hook kn;
-	id
+    if Lib.is_modtype () then
+      begin
+	let cst = Declare.declare_internal_constant id
+	  (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
+	in
+	  Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps;
+	  Typeclasses.add_instance { is_class = k ; is_pri = None; is_impl = cst };
+	  Command.assumption_message id;
+	  (match hook with Some h -> h cst | None -> ()); id
+      end
     else
-      let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-	Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false);
-	Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
-	  (!refine_ref (evm, term));
-	Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
-	id
-     
+      begin
+	let subst, _propsctx = 
+	  let props = 
+	    List.map (fun (x, l, d) -> 
+	      x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
+	      props
+	  in
+	    if List.length props > List.length k.cl_props then 
+	      mismatched_props env' (List.map snd props) k.cl_props;
+	    let props, rest = 
+	      List.fold_left
+		(fun (props, rest) (id,_,_) -> 
+		  try 
+		    let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
+		    let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+		      c :: props, rest'
+		  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))
+	      else
+		type_ctx_instance isevars env' k.cl_props props substctx
+	in
+	let app = inst_constr (List.rev_map snd subst) in 
+	let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
+	isevars := Evarutil.nf_evar_defs !isevars;
+	let term = Evarutil.nf_isevar !isevars term in
+	let hook cst = 
+	  let inst = 
+	    { is_class = k;
+	      is_pri = pri;
+	      is_impl = cst;
+	    }
+	  in
+	    Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps;
+	    Typeclasses.add_instance inst;
+	    (match hook with Some h -> h cst | None -> ())
+	in
+	let evm = Evd.evars_of (undefined_evars !isevars) in
+	  if evm = Evd.empty then
+	    let cdecl = 
+	      let kind = IsDefinition Instance in
+	      let entry = 
+		{ const_entry_body   = term;
+		  const_entry_type   = Some termtype;
+		  const_entry_opaque = false;
+		  const_entry_boxed  = false }
+	      in DefinitionEntry entry, kind
+	    in
+	    let kn = Declare.declare_constant id cdecl in
+	      Flags.if_verbose Command.definition_message id;
+	      hook kn;
+	      id
+	  else
+	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+	      Flags.silently (fun () ->
+		Command.start_proof id kind termtype (fun _ -> function ConstRef cst -> hook cst | _ -> assert false);
+		Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS (Evd.evars_of !isevars)) *)
+		  (!refine_ref (evm, term));
+		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
+	      Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
+	      id
+      end
+
 let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
 
 let solve_by_tac env evd evar evi t =
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 6671eed72..973845d9c 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -43,8 +43,9 @@ val new_instance :
   local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
+  ?tac:Proof_type.tactic  ->
+  ?hook:(constant -> unit) ->
   int option ->
-  (constant -> unit) ->
   identifier
 
 (* For generation on names based on classes only *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index a6a403c03..31420d189 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -33,6 +33,7 @@ open Redexpr
 val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit
 
 val definition_message : identifier -> unit
+val assumption_message : identifier -> unit
 
 val declare_definition : identifier -> definition_kind ->
   local_binder list -> red_expr option -> constr_expr ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4e2901319..1ea732add 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -537,7 +537,7 @@ let vernac_class id par ar sup props =
   Classes.new_class id par ar sup props
 
 let vernac_instance sup inst props pri =
-  ignore(Classes.new_instance sup inst props pri (fun _ -> ()))
+  ignore(Classes.new_instance sup inst props pri)
 
 let vernac_context l =
   Classes.context l