Annotations at functor applications:

 - The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]"
 - The earlier syntax !F X should now be written "F X [no inline]"
   (note that using ! is still possible for compatibility)
 - A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute
   foo_scope by bar_scope in all arguments scope of objects in F.

 BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier.
 Arguments scope for lemmas are fixed for instances of Numbers.

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

8 files changed, 54 insertions, 126 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 583491386..9748a4366 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -24,65 +24,24 @@ Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
 *)
 
+Delimit Scope bigZ_scope with bigZ.
 
 Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
- ZMake.Make BigN <+ ZTypeIsZAxioms <+ !ZProp <+ HasEqBool2Dec
- <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
+ ZMake.Make BigN [scope abstract_scope to bigZ_scope]
+ <+ ZTypeIsZAxioms [scope abstract_scope to bigZ_scope]
+ <+ ZProp [no inline, scope abstract_scope to bigZ_scope]
+ <+ HasEqBool2Dec [no inline, scope abstract_scope to bigZ_scope]
+ <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigZ_scope]
+ <+ MinMaxDecProperties [no inline, scope abstract_scope to bigZ_scope].
 
 (** Notations about [BigZ] *)
 
-Notation bigZ := BigZ.t.
+Local Open Scope bigZ_scope.
 
-Delimit Scope bigZ_scope with bigZ.
-Bind Scope bigZ_scope with bigZ.
-Bind Scope bigZ_scope with BigZ.t.
-Bind Scope bigZ_scope with BigZ.t_.
-(* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
+Notation bigZ := BigZ.t.
+Bind Scope bigZ_scope with bigZ BigZ.t BigZ.t_.
 Arguments Scope BigZ.Pos [bigN_scope].
 Arguments Scope BigZ.Neg [bigN_scope].
-Arguments Scope BigZ.to_Z [bigZ_scope].
-Arguments Scope BigZ.succ [bigZ_scope].
-Arguments Scope BigZ.pred [bigZ_scope].
-Arguments Scope BigZ.opp [bigZ_scope].
-Arguments Scope BigZ.square [bigZ_scope].
-Arguments Scope BigZ.add [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.sub [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.mul [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.div [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.eq [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.lt [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.le [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.eq [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.compare [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.min [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.max [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.eq_bool [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.pow_pos [bigZ_scope positive_scope].
-Arguments Scope BigZ.pow_N [bigZ_scope N_scope].
-Arguments Scope BigZ.pow [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.log2 [bigZ_scope].
-Arguments Scope BigZ.sqrt [bigZ_scope].
-Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.quot [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.rem [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.lcm [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.even [bigZ_scope].
-Arguments Scope BigZ.odd [bigZ_scope].
-Arguments Scope BigN.testbit [bigZ_scope bigZ_scope].
-Arguments Scope BigN.shiftl [bigZ_scope bigZ_scope].
-Arguments Scope BigN.shiftr [bigZ_scope bigZ_scope].
-Arguments Scope BigN.lor [bigZ_scope bigZ_scope].
-Arguments Scope BigN.land [bigZ_scope bigZ_scope].
-Arguments Scope BigN.ldiff [bigZ_scope bigZ_scope].
-Arguments Scope BigN.lxor [bigZ_scope bigZ_scope].
-Arguments Scope BigN.setbit [bigZ_scope bigZ_scope].
-Arguments Scope BigN.clearbit [bigZ_scope bigZ_scope].
-Arguments Scope BigN.lnot [bigZ_scope].
-Arguments Scope BigN.div2 [bigZ_scope].
-Arguments Scope BigN.ones [bigZ_scope].
-
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Local Notation "1" := BigZ.one : bigZ_scope.
 Local Notation "2" := BigZ.two : bigZ_scope.
@@ -94,21 +53,19 @@ Infix "/" := BigZ.div : bigZ_scope.
 Infix "^" := BigZ.pow : bigZ_scope.
 Infix "?=" := BigZ.compare : bigZ_scope.
 Infix "==" := BigZ.eq (at level 70, no associativity) : bigZ_scope.
-Notation "x != y" := (~x==y)%bigZ (at level 70, no associativity) : bigZ_scope.
+Notation "x != y" := (~x==y) (at level 70, no associativity) : bigZ_scope.
 Infix "<" := BigZ.lt : bigZ_scope.
 Infix "<=" := BigZ.le : bigZ_scope.
-Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
-Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
-Notation "x < y < z" := (x<y /\ y<z)%bigZ : bigZ_scope.
-Notation "x < y <= z" := (x<y /\ y<=z)%bigZ : bigZ_scope.
-Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
-Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
+Notation "x > y" := (y < x) (only parsing) : bigZ_scope.
+Notation "x >= y" := (y <= x) (only parsing) : bigZ_scope.
+Notation "x < y < z" := (x<y /\ y<z) : bigZ_scope.
+Notation "x < y <= z" := (x<y /\ y<=z) : bigZ_scope.
+Notation "x <= y < z" := (x<=y /\ y<z) : bigZ_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z) : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
 Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
 Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
 
-Local Open Scope bigZ_scope.
-
 (** Some additional results about [BigZ] *)
 
 Theorem spec_to_Z: forall n : bigZ,
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 7534628fa..57b98e860 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -29,6 +29,8 @@ Module Make (N:NType) <: ZType.
 
  Definition t := t_.
 
+ Bind Scope abstract_scope with t t_.
+
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
  Definition two := Pos N.two.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 366418035..fbb91ef7f 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -223,8 +223,9 @@ Definition eq := (@eq Z).
 
 (** Now the generic properties. *)
 
-Include ZProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include ZProp [scope abstract_scope to Z_scope]
+ <+ UsualMinMaxLogicalProperties [scope abstract_scope to Z_scope]
+ <+ UsualMinMaxDecProperties [scope abstract_scope to Z_scope].
 
 End Z.
 
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 56fad9347..65b646356 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -12,6 +12,11 @@ Require Import NZAxioms.
 
 Module Type NZBaseProp (Import NZ : NZDomainSig').
 
+(** An artificial scope meant to be substituted later *)
+
+Delimit Scope abstract_scope with abstract.
+Bind Scope abstract_scope with t.
+
 Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
 
 Lemma eq_sym_iff : forall x y, x==y <-> y==x.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 315876656..858c06658 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -26,62 +26,23 @@ Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
 
 *)
 
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
- NMake.Make Int31Cyclic <+ NTypeIsNAxioms
- <+ !NProp <+ HasEqBool2Dec
- <+ !MinMaxLogicalProperties <+ !MinMaxDecProperties.
+Delimit Scope bigN_scope with bigN.
 
+Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
+ NMake.Make Int31Cyclic [scope abstract_scope to bigN_scope]
+ <+ NTypeIsNAxioms [scope abstract_scope to bigN_scope]
+ <+ NProp [no inline, scope abstract_scope to bigN_scope]
+ <+ HasEqBool2Dec [no inline, scope abstract_scope to bigN_scope]
+ <+ MinMaxLogicalProperties [no inline, scope abstract_scope to bigN_scope]
+ <+ MinMaxDecProperties [no inline, scope abstract_scope to bigN_scope].
 
 (** Notations about [BigN] *)
 
-Notation bigN := BigN.t.
-
-Delimit Scope bigN_scope with bigN.
-Bind Scope bigN_scope with bigN.
-Bind Scope bigN_scope with BigN.t.
-Bind Scope bigN_scope with BigN.t'.
-(* Bind Scope has no retroactive effect, let's declare scopes by hand. *)
-Arguments Scope BigN.to_Z [bigN_scope].
-Arguments Scope BigN.to_N [bigN_scope].
-Arguments Scope BigN.succ [bigN_scope].
-Arguments Scope BigN.pred [bigN_scope].
-Arguments Scope BigN.square [bigN_scope].
-Arguments Scope BigN.add [bigN_scope bigN_scope].
-Arguments Scope BigN.sub [bigN_scope bigN_scope].
-Arguments Scope BigN.mul [bigN_scope bigN_scope].
-Arguments Scope BigN.div [bigN_scope bigN_scope].
-Arguments Scope BigN.eq [bigN_scope bigN_scope].
-Arguments Scope BigN.lt [bigN_scope bigN_scope].
-Arguments Scope BigN.le [bigN_scope bigN_scope].
-Arguments Scope BigN.eq [bigN_scope bigN_scope].
-Arguments Scope BigN.compare [bigN_scope bigN_scope].
-Arguments Scope BigN.min [bigN_scope bigN_scope].
-Arguments Scope BigN.max [bigN_scope bigN_scope].
-Arguments Scope BigN.eq_bool [bigN_scope bigN_scope].
-Arguments Scope BigN.pow_pos [bigN_scope positive_scope].
-Arguments Scope BigN.pow_N [bigN_scope N_scope].
-Arguments Scope BigN.pow [bigN_scope bigN_scope].
-Arguments Scope BigN.log2 [bigN_scope].
-Arguments Scope BigN.sqrt [bigN_scope].
-Arguments Scope BigN.div_eucl [bigN_scope bigN_scope].
-Arguments Scope BigN.modulo [bigN_scope bigN_scope].
-Arguments Scope BigN.gcd [bigN_scope bigN_scope].
-Arguments Scope BigN.lcm [bigN_scope bigN_scope].
-Arguments Scope BigN.even [bigN_scope].
-Arguments Scope BigN.odd [bigN_scope].
-Arguments Scope BigN.testbit [bigN_scope bigN_scope].
-Arguments Scope BigN.shiftl [bigN_scope bigN_scope].
-Arguments Scope BigN.shiftr [bigN_scope bigN_scope].
-Arguments Scope BigN.lor [bigN_scope bigN_scope].
-Arguments Scope BigN.land [bigN_scope bigN_scope].
-Arguments Scope BigN.ldiff [bigN_scope bigN_scope].
-Arguments Scope BigN.lxor [bigN_scope bigN_scope].
-Arguments Scope BigN.setbit [bigN_scope bigN_scope].
-Arguments Scope BigN.clearbit [bigN_scope bigN_scope].
-Arguments Scope BigN.lnot [bigN_scope bigN_scope].
-Arguments Scope BigN.div2 [bigN_scope].
-Arguments Scope BigN.ones [bigN_scope].
+Local Open Scope bigN_scope.
 
+Notation bigN := BigN.t.
+Bind Scope bigN_scope with bigN BigN.t BigN.t'.
+Arguments Scope BigN.N0 [int31_scope].
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
 Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)
@@ -92,20 +53,18 @@ Infix "/" := BigN.div : bigN_scope.
 Infix "^" := BigN.pow : bigN_scope.
 Infix "?=" := BigN.compare : bigN_scope.
 Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
-Notation "x != y" := (~x==y)%bigN (at level 70, no associativity) : bigN_scope.
+Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope.
 Infix "<" := BigN.lt : bigN_scope.
 Infix "<=" := BigN.le : bigN_scope.
-Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
-Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
-Notation "x < y < z" := (x<y /\ y<z)%bigN : bigN_scope.
-Notation "x < y <= z" := (x<y /\ y<=z)%bigN : bigN_scope.
-Notation "x <= y < z" := (x<=y /\ y<z)%bigN : bigN_scope.
-Notation "x <= y <= z" := (x<=y /\ y<=z)%bigN : bigN_scope.
+Notation "x > y" := (y < x) (only parsing) : bigN_scope.
+Notation "x >= y" := (y <= x) (only parsing) : bigN_scope.
+Notation "x < y < z" := (x<y /\ y<z) : bigN_scope.
+Notation "x < y <= z" := (x<y /\ y<=z) : bigN_scope.
+Notation "x <= y < z" := (x<=y /\ y<z) : bigN_scope.
+Notation "x <= y <= z" := (x<=y /\ y<=z) : bigN_scope.
 Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
 Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope.
 
-Local Open Scope bigN_scope.
-
 (** Example of reasoning about [BigN] *)
 
 Theorem succ_pred: forall q : bigN,
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index b5cc4c51d..f095a3482 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -138,6 +138,8 @@ pr
   pr "";
   pr " Definition t := t'.";
   pr "";
+  pr " Bind Scope abstract_scope with t t'.";
+  pr "";
 
   pr " (** * A generic toolbox for building and deconstructing [t] *)";
   pr "";
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index bd59ef494..cf284a2f1 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -234,8 +234,9 @@ Definition lor := Nor.
 Definition ldiff := Ndiff.
 Definition div2 := Ndiv2.
 
-Include NProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include NProp [scope abstract_scope to N_scope]
+ <+ UsualMinMaxLogicalProperties [scope abstract_scope to N_scope]
+ <+ UsualMinMaxDecProperties [scope abstract_scope to N_scope].
 
 End N.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 0cf9ae441..4578851e2 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -756,8 +756,9 @@ Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _.
 
 (** Generic Properties *)
 
-Include NProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include NProp [scope abstract_scope to nat_scope]
+ <+ UsualMinMaxLogicalProperties [scope abstract_scope to nat_scope]
+ <+ UsualMinMaxDecProperties [scope abstract_scope to nat_scope].
 
 End Nat.