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

8 files changed, 18 insertions, 18 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 4acb45401d..4b3d18be4b 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 0f15e9a299..2ec1cc9b04 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 b4a8a4203a..4736312939 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 fe2b262f21..2522f70c12 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 ff220e7933..f6328e2498 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 62eee289d3..1be2f85087 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 bdabb1086d..1cb4746741 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 9ff9c08cf2..1aa10958f0 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.