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

3 files changed, 8 insertions, 8 deletions

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).