More dynamic argument scopes

 When arguments scopes are set manually, nothing new, they stay
 as they are (until maybe another Arguments invocation).
 But when argument scopes are computed out of the argument type and
 the Bind Scope information, this kind of scope is now dynamic:
 a later Bind Scope will be able to impact the scopes of an earlier
 constant. For Instance:

 Definition f (n:nat) := n.
 About f. (* Argument scope is [nat_scope] *)
 Bind Scope other_scope with nat.
 About f. (* Argument scope is [other_scope] *)

 This allows to get rid of hacks for modifying scopes during functor
 applications. Moreover, the subst_arguments_scope is now
 environment-insensitive (needed for forthcoming changes in declaremods).

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

1 files changed, 62 insertions, 0 deletions

diff --git a/test-suite/success/NumberScopes.v b/test-suite/success/NumberScopes.v
new file mode 100644
index 0000000000..ca9457be7c
--- /dev/null
+++ b/test-suite/success/NumberScopes.v
@@ -0,0 +1,62 @@
+
+(* We check that various definitions or lemmas have the correct
+   argument scopes, especially the ones created via functor application. *)
+
+Close Scope nat_scope.
+
+Require Import PArith.
+Check (Pos.add 1 2).
+Check (Pos.add_comm 1 2).
+Check (Pos.min_comm 1 2).
+Definition f_pos (x:positive) := x.
+Definition f_pos' (x:Pos.t) := x.
+Check (f_pos 1).
+Check (f_pos' 1).
+
+Require Import ZArith.
+Check (Z.add 1 2).
+Check (Z.add_comm 1 2).
+Check (Z.min_comm 1 2).
+Definition f_Z (x:Z) := x.
+Definition f_Z' (x:Z.t) := x.
+Check (f_Z 1).
+Check (f_Z' 1).
+
+Require Import NArith.
+Check (N.add 1 2).
+Check (N.add_comm 1 2).
+Check (N.min_comm 1 2).
+Definition f_N (x:N) := x.
+Definition f_N' (x:N.t) := x.
+Check (f_N 1).
+Check (f_N' 1).
+
+Require Import NPeano.
+Check (Nat.add 1 2).
+Check (Nat.add_comm 1 2).
+Check (Nat.min_comm 1 2).
+Definition f_nat (x:nat) := x.
+Definition f_nat' (x:Nat.t) := x.
+Check (f_nat 1).
+Check (f_nat' 1).
+
+Require Import BigN.
+Check (BigN.add 1 2).
+Check (BigN.add_comm 1 2).
+Check (BigN.min_comm 1 2).
+Definition f_bigN (x:bigN) := x.
+Check (f_bigN 1).
+
+Require Import BigZ.
+Check (BigZ.add 1 2).
+Check (BigZ.add_comm 1 2).
+Check (BigZ.min_comm 1 2).
+Definition f_bigZ (x:bigZ) := x.
+Check (f_bigZ 1).
+
+Require Import BigQ.
+Check (BigQ.add 1 2).
+Check (BigQ.add_comm 1 2).
+Check (BigQ.min_comm 1 2).
+Definition f_bigQ (x:bigQ) := x.
+Check (f_bigQ 1).
\ No newline at end of file