Documentation Prop<=Set et Arguments Scope Global

Correction au passage d'un bug de Arguments Scope Global


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

2 files changed, 85 insertions, 0 deletions

diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
new file mode 100644
index 0000000000..6643c1429a
--- /dev/null
+++ b/test-suite/output/ArgumentsScope.out
@@ -0,0 +1,56 @@
+a : bool -> bool
+
+Argument scope is [bool_scope]
+Expands to: Variable a
+b : bool -> bool
+
+Argument scope is [bool_scope]
+Expands to: Variable b
+negb'' : bool -> bool
+
+Argument scope is [bool_scope]
+negb'' is transparent
+Expands to: Constant Top.A.B.negb''
+negb' : bool -> bool
+
+Argument scope is [bool_scope]
+negb' is transparent
+Expands to: Constant Top.A.negb'
+negb : bool -> bool
+
+Argument scope is [bool_scope]
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+a : bool -> bool
+
+Expands to: Variable a
+b : bool -> bool
+
+Expands to: Variable b
+negb : bool -> bool
+
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+negb' : bool -> bool
+
+negb' is transparent
+Expands to: Constant Top.A.negb'
+negb'' : bool -> bool
+
+negb'' is transparent
+Expands to: Constant Top.A.B.negb''
+a : bool -> bool
+
+Expands to: Variable a
+negb : bool -> bool
+
+negb is transparent
+Expands to: Constant Coq.Init.Datatypes.negb
+negb' : bool -> bool
+
+negb' is transparent
+Expands to: Constant Top.negb'
+negb'' : bool -> bool
+
+negb'' is transparent
+Expands to: Constant Top.negb''
diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
new file mode 100644
index 0000000000..13b5e13dd2
--- /dev/null
+++ b/test-suite/output/ArgumentsScope.v
@@ -0,0 +1,29 @@
+(* A few tests to check Argument Scope Global command *)
+
+Section A.
+Variable a : bool -> bool.
+Definition negb' := negb.
+Section B.
+Variable b : bool -> bool.
+Definition negb'' := negb.
+About a.
+About b.
+About negb''.
+About negb'.
+About negb.
+Arguments Scope Global negb'' [ _ ].
+Arguments Scope Global negb' [ _ ].
+Arguments Scope Global negb [ _ ].
+Arguments Scope Global a [ _ ].
+Arguments Scope Global b [ _ ].
+About a.
+About b.
+About negb.
+About negb'.
+About negb''.
+End B.
+About a.
+End A.
+About negb.
+About negb'.
+About negb''.