Specific syntax for Instances in Module Type: Declare Instance

NB: the grammar entry is placed in vernac:command on purpose
 even if it should have gone into vernac:gallina_ext. Camlp4
 isn't factorising rules starting by "Declare" in a correct way
 otherwise...

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

21 files changed, 94 insertions, 74 deletions

diff --git a/CHANGES b/CHANGES
index 9fdbc6ab0..fb4e921d1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -88,7 +88,9 @@ Vernacular commands
   congruence schemes available to user (governed by options "Unset
   Case Analysis Schemes" and "Unset Congruence Schemes").
 - Fixpoint/CoFixpoint now support building part or all of bodies using tactics.
-
+- Declaring axiomatic type class instances in Module Type should be now
+  done via new command "Declare Instance", while the syntax "Instance"
+  now always provides a concrete instance, both in and out of Module Type.
 
 Tools
 
@@ -143,7 +145,7 @@ Language
 - New implementation of the module system. The sharing between non-logical
   object and the management of the name-space has been improved by the new 
   \Delta-equivalence on qualified name. The include operator has been extended 
-  to high-order structures (cf. libraries Numbers ans Structures to see examples).
+  to high-order structures (cf. libraries Numbers and Structures to see examples).
   Interactive proofs are now authorized in module type.
 
 Changes from V8.1 to V8.2
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 0ddbb6d89..1ea07f79a 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -340,6 +340,14 @@ priority as for auto hints.
 \item {\tt Program Instance} \comindex{Program Instance}
   Switches the type-checking to \Program~(chapter \ref{Program})
   and uses the obligation mechanism to manage missing fields.
+
+\item {\tt Declare Instance} \comindex{Declare Instance}
+  In a {\tt Module Type}, this command states that a corresponding
+  concrete instance should exist in any implementation of this
+  {\tt Module Type}. This is similar to the distinction between
+  {\tt Parameter} vs. {\tt Definition}, or between {\tt Declare Module}
+  and {\tt Module}.
+
 \end{Variants}
 
 Besides the {\tt Class} and {\tt Instance} vernacular commands, there
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3baed8992..4672a732a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -50,6 +50,7 @@ let decl_notation = Gram.Entry.create "vernac:decl_notation"
 let typeclass_context = Gram.Entry.create "vernac:typeclass_context"
 let record_field = Gram.Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Gram.Entry.create "vernac:of_type_with_opt_coercion"
+let instance_name = Gram.Entry.create "vernac:instance_name"
 
 let get_command_entry () =
   match Decl_mode.get_current_mode () with
@@ -463,7 +464,7 @@ END
 
 (* Extensions: implicits, coercions, etc. *)
 GEXTEND Gram
-  GLOBAL: gallina_ext;
+  GLOBAL: gallina_ext instance_name;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
@@ -515,28 +516,13 @@ GEXTEND Gram
       | IDENT "Context"; c = binders_let ->
 	  VernacContext c
 
-      | IDENT "Instance"; ":";
+      | IDENT "Instance"; namesup = instance_name; ":";
 	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> r |
 	     ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
-	   VernacInstance (not (use_section_locality ()), [], ((loc,Anonymous), expl, t), props, pri)
-
-      | IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
-	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
-	 pri = OPT [ "|"; i = natural -> i ] ;
-	 props = [ ":="; "{"; r = record_declaration; "}" -> r |
-	     ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
-	   let sup =
-	     match sup with
-		 None -> []
-	       | Some l -> l
-	   in
-	   let n =
-	     let (loc, id) = name in
-	       (loc, Name id)
-	   in
-	     VernacInstance (not (use_non_locality ()), sup, (n, expl, t), props, pri)
+	   VernacInstance (false, not (use_non_locality ()),
+			   snd namesup, (fst namesup, expl, t), props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = global -> 
 	  VernacDeclareInstance (not (use_section_locality ()), is)
@@ -572,6 +558,13 @@ GEXTEND Gram
       | "-"; n=INT -> Conv_oracle.Level (- int_of_string n)
       | IDENT "transparent" -> Conv_oracle.transparent ] ]
   ;
+  instance_name:
+    [ [ name = identref; sup = OPT binders_let ->
+	  (let (loc,id) = name in (loc, Name id)),
+          (Option.default [] sup)
+      | -> (loc, Anonymous), []  ] ]
+  ;
+
 END
 
 GEXTEND Gram
@@ -580,6 +573,14 @@ GEXTEND Gram
   command:
     [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l
 
+      (* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
+      | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
+	 expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
+	 pri = OPT [ "|"; i = natural -> i ] ->
+	   VernacInstance (true, not (use_non_locality ()),
+			   snd namesup, (fst namesup, expl, t),
+			   CRecord (loc, None, []), pri)
+
       (* System directory *)
       | IDENT "Pwd" -> VernacChdir None
       | IDENT "Cd" -> VernacChdir None
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 873558dff..4b1162dbd 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -719,9 +719,10 @@ let rec pr_vernac = function
 (* 	  prlist_with_sep (fun () -> str";" ++ spc())  *)
 (* 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) *)
 
- | VernacInstance (glob, sup, (instid, bk, cl), props, pri) ->
+ | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
      hov 1 (
        pr_non_locality (not glob) ++
+       (if abst then str"Declare " else mt ()) ++
        str"Instance" ++ spc () ++
 	 pr_and_type_binders_arg sup ++
 	 str"=>" ++ spc () ++
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index b337d3352..0eba0f633 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -169,8 +169,10 @@ let subtac (loc, command) =
   | VernacAssumption (stre,nl,l) ->
       vernac_assumption env isevars stre l nl
 
-  | VernacInstance (glob, sup, is, props, pri) ->
+  | VernacInstance (abst, glob, sup, is, props, pri) ->
       dump_constraint "inst" is;
+      if abst then
+	error "Declare Instance not supported here.";
       ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 
   | VernacCoFixpoint (l, b) ->
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index ec432de83..fbaa01c90 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -128,7 +128,7 @@ Module Type WSetsOn (E : DecidableType).
 
   (** Logical predicates *)
   Parameter In : elt -> t -> Prop.
-  Instance In_compat : Proper (E.eq==>eq==>iff) In.
+  Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.
 
   Definition Equal s s' := forall a : elt, In a s <-> In a s'.
   Definition Subset s s' := forall a : elt, In a s -> In a s'.
@@ -140,7 +140,7 @@ Module Type WSetsOn (E : DecidableType).
   Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).
 
   Definition eq : t -> t -> Prop := Equal.
-  Instance eq_equiv : Equivalence eq. (* obvious, for subtyping only *)
+  Declare Instance eq_equiv : Equivalence eq. (* obvious, for subtyping only *)
   Parameter eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.
 
   (** Specifications of set operators *)
@@ -220,8 +220,8 @@ Module Type SetsOn (E : OrderedType).
   Parameter lt : t -> t -> Prop.
 
   (** Specification of [lt] *)
-  Instance lt_strorder : StrictOrder lt.
-  Instance lt_compat : Proper (eq==>eq==>iff) lt.
+  Declare Instance lt_strorder : StrictOrder lt.
+  Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
   Section Spec.
   Variable s s': t.
@@ -342,11 +342,11 @@ Module Type WRawSets (E : DecidableType).
       predicate [Ok]. If [Ok] isn't decidable, [isok] may be the
       always-false function. *)
   Parameter isok : t -> bool.
-  Instance isok_Ok s `(isok s = true) : Ok s | 10.
+  Declare Instance isok_Ok s `(isok s = true) : Ok s | 10.
 
   (** Logical predicates *)
   Parameter In : elt -> t -> Prop.
-  Instance In_compat : Proper (E.eq==>eq==>iff) In.
+  Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.
 
   Definition Equal s s' := forall a : elt, In a s <-> In a s'.
   Definition Subset s s' := forall a : elt, In a s -> In a s'.
@@ -358,20 +358,20 @@ Module Type WRawSets (E : DecidableType).
   Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).
 
   Definition eq : t -> t -> Prop := Equal.
-  Instance eq_equiv : Equivalence eq.
+  Declare Instance eq_equiv : Equivalence eq.
 
   (** First, all operations are compatible with the well-formed predicate. *)
 
-  Instance empty_ok : Ok empty.
-  Instance add_ok s x `(Ok s) : Ok (add x s).
-  Instance remove_ok s x `(Ok s) : Ok (remove x s).
-  Instance singleton_ok x : Ok (singleton x).
-  Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
-  Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
-  Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
-  Instance filter_ok s f `(Ok s) : Ok (filter f s).
-  Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
-  Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
+  Declare Instance empty_ok : Ok empty.
+  Declare Instance add_ok s x `(Ok s) : Ok (add x s).
+  Declare Instance remove_ok s x `(Ok s) : Ok (remove x s).
+  Declare Instance singleton_ok x : Ok (singleton x).
+  Declare Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
+  Declare Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
+  Declare Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
+  Declare Instance filter_ok s f `(Ok s) : Ok (filter f s).
+  Declare Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
+  Declare Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).
 
   (** Now, the specifications, with constraints on the input sets. *)
 
@@ -562,8 +562,8 @@ Module Type RawSets (E : OrderedType).
   Parameter lt : t -> t -> Prop.
 
   (** Specification of [lt] *)
-  Instance lt_strorder : StrictOrder lt.
-  Instance lt_compat : Proper (eq==>eq==>iff) lt.
+  Declare Instance lt_strorder : StrictOrder lt.
+  Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
   Section Spec.
   Variable s s': t.
@@ -674,7 +674,7 @@ End Raw2Sets.
 Module Type IN (O:OrderedType).
  Parameter Inline t : Type.
  Parameter Inline In : O.t -> t -> Prop.
- Instance In_compat : Proper (O.eq==>eq==>iff) In.
+ Declare Instance In_compat : Proper (O.eq==>eq==>iff) In.
  Definition Equal s s' := forall x, In x s <-> In x s'.
  Definition Empty s := forall x, ~In x s.
 End IN.
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 4acb45401..4b3d18be4 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -19,7 +19,7 @@ Include Type NZOrdAxiomsSig.
 Local Open Scope NumScope.
 
 Parameter Inline opp : t -> t.
-Instance opp_wd : Proper (eq==>eq) opp.
+Declare Instance opp_wd : Proper (eq==>eq) opp.
 
 Notation "- x" := (opp x) (at level 35, right associativity) : NumScope.
 Notation "- 1" := (- (1)) : NumScope.
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 0f15e9a29..2ec1cc9b0 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -33,8 +33,8 @@ Module Type ZDiv (Import Z : ZAxiomsSig).
  Infix "/" := div : NumScope.
  Infix "mod" := modulo (at level 40, no associativity) : NumScope.
 
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
  Definition abs z := max z (-z).
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index b4a8a4203..473631293 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -36,8 +36,8 @@ Module Type ZDiv (Import Z : ZAxiomsSig).
  Infix "/" := div : NumScope.
  Infix "mod" := modulo (at level 40, no associativity) : NumScope.
 
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
  Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
  Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b.
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index fe2b262f2..2522f70c1 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -36,8 +36,8 @@ Module Type ZDiv (Import Z : ZAxiomsSig).
  Infix "/" := div : NumScope.
  Infix "mod" := modulo (at level 40, no associativity) : NumScope.
 
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
  Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
  Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index ff220e793..f6328e249 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -37,8 +37,8 @@ Notation S := succ.
 Notation P := pred.
 Notation "1" := (S 0) : NumScope.
 
-Instance succ_wd : Proper (eq ==> eq) S.
-Instance pred_wd : Proper (eq ==> eq) P.
+Declare Instance succ_wd : Proper (eq ==> eq) S.
+Declare Instance pred_wd : Proper (eq ==> eq) P.
 
 Axiom pred_succ : forall n, P (S n) == n.
 
@@ -67,9 +67,9 @@ Notation "x + y" := (add x y) : NumScope.
 Notation "x - y" := (sub x y) : NumScope.
 Notation "x * y" := (mul x y) : NumScope.
 
-Instance add_wd : Proper (eq ==> eq ==> eq) add.
-Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
-Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
+Declare Instance add_wd : Proper (eq ==> eq ==> eq) add.
+Declare Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
+Declare Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
 
 Axiom add_0_l : forall n, (0 + n) == n.
 Axiom add_succ_l : forall n m, (S n) + m == S (n + m).
@@ -107,7 +107,7 @@ Notation "x <= y <= z" := (x<=y /\ y<=z) : NumScope.
 Notation "x <= y < z" := (x<=y /\ y<z) : NumScope.
 Notation "x < y <= z" := (x<y /\ y<=z) : NumScope.
 
-Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
+Declare Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
 (** Compatibility of [le] can be proved later from [lt_wd]
     and [lt_eq_cases] *)
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 62eee289d..1be2f8508 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -20,8 +20,8 @@ Module Type NZDiv (Import NZ : NZOrdAxiomsSig).
  Infix "/" := div : NumScope.
  Infix "mod" := modulo (at level 40, no associativity) : NumScope.
 
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
  Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
  Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index bdabb1086..1cb474674 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -23,7 +23,7 @@ Axiom pred_0 : P 0 == 0.
 Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A.
 Implicit Arguments recursion [A].
 
-Instance recursion_wd (A : Type) (Aeq : relation A) :
+Declare Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 
 Axiom recursion_0 :
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 9ff9c08cf..1aa10958f 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -20,8 +20,8 @@ Module Type NDiv (Import N : NAxiomsSig).
  Infix "/" := div : NumScope.
  Infix "mod" := modulo (at level 40, no associativity) : NumScope.
 
- Instance div_wd : Proper (eq==>eq==>eq) div.
- Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+ Declare Instance div_wd : Proper (eq==>eq==>eq) div.
+ Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
  Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
  Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b.
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 087a6a7dd..0957ef243 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -23,7 +23,7 @@ End BareEquality.
 (** * Specification of the equality by the Type Classe [Equivalence] *)
 
 Module Type IsEq (Import E:BareEquality).
-  Instance eq_equiv : Equivalence eq.
+  Declare Instance eq_equiv : Equivalence eq.
   Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv).
   Hint Resolve (@Equivalence_Transitive _ _ eq_equiv).
   Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv).
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index 8a3635686..f75e1ae91 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -31,9 +31,9 @@ Module Type OrderSig.
 
 Parameter Inline t : Type.
 Parameters eq lt le : t -> t -> Prop.
-Instance eq_equiv : Equivalence eq.
-Instance lt_strorder : StrictOrder lt.
-Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Declare Instance eq_equiv : Equivalence eq.
+Declare Instance lt_strorder : StrictOrder lt.
+Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
 Parameter lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
 Parameter le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
 
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 310f99a4a..be7ec153b 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -18,8 +18,8 @@ Module Type MiniOrderedType.
   Include Type EqualityType.
 
   Parameter Inline lt : t -> t -> Prop.
-  Instance lt_strorder : StrictOrder lt.
-  Instance lt_compat : Proper (eq==>eq==>iff) lt.
+  Declare Instance lt_strorder : StrictOrder lt.
+  Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
   Parameter Inline compare : t -> t -> comparison.
   Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
@@ -63,10 +63,10 @@ Module Type UsualOrderedType.
  Include Type UsualDecidableType.
 
  Parameter Inline lt : t -> t -> Prop.
- Instance lt_strorder : StrictOrder lt.
+ Declare Instance lt_strorder : StrictOrder lt.
  (* The following is useless since eq is Leibniz, but should be there
     for subtyping... *)
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
+ Declare Instance lt_compat : Proper (eq==>eq==>iff) lt.
 
  Parameter Inline compare : t -> t -> comparison.
  Axiom compare_spec : forall x y, CompSpec eq lt x y (compare x y).
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 590f5c6f4..ca16e2131 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -128,7 +128,8 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
-let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
+let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
+    ?(generalize=true)
     ?(tac:Proof_type.tactic option) ?(hook:(global_reference -> unit) option) pri =
   let env = Global.env() in
   let evars = ref Evd.empty in
@@ -179,8 +180,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
   evars := resolve_typeclasses env !evars;
   let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
-    if Lib.is_modtype () then
+    if abstract then
       begin
+	if not (Lib.is_modtype ()) then
+	  error "Declare Instance while not in Module Type.";
 	let _, ty_constr = instance_constructor k (List.rev subst) in
 	let termtype =
 	  let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index c8439a166..b8b104d47 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -50,6 +50,7 @@ val declare_instance_constant :
   Names.identifier
 
 val new_instance :
+  ?abstract:bool -> (* Not abstract by default. *)
   ?global:bool -> (* Not global by default. *)
   local_binder list ->
   typeclass_constraint ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a90136d43..7955d4916 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -611,9 +611,9 @@ let vernac_identity_coercion stre id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance glob sup inst props pri =
+let vernac_instance abst glob sup inst props pri =
   Dumpglob.dump_constraint inst false "inst";
-  ignore(Classes.new_instance ~global:glob sup inst props pri)
+  ignore(Classes.new_instance ~abstract:abst ~global:glob sup inst props pri)
 
 let vernac_context l =
   List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
@@ -1340,7 +1340,8 @@ let interp c = match c with
   | VernacIdentityCoercion (str,(_,id),s,t) -> vernac_identity_coercion str id s t
 
   (* Type classes *)
-  | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
+  | VernacInstance (abst, glob, sup, inst, props, pri) ->
+      vernac_instance abst glob sup inst props pri
   | VernacContext sup -> vernac_context sup
   | VernacDeclareInstance (glob, id) -> vernac_declare_instance glob id
   | VernacDeclareClass id -> vernac_declare_class id
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 5be5c940b..2df396e09 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -248,6 +248,7 @@ type vernac_expr =
 
   (* Type classes *)
   | VernacInstance of
+      bool * (* abstract instance *)
       bool * (* global *)
       local_binder list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)