From 7f110df7d7ff6a4d43f3c8d19305b20e24f4800e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 1 Jul 2008 21:59:00 +0000
Subject: 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
---
 test-suite/output/ArgumentsScope.out | 56 ++++++++++++++++++++++++++++++++++++
 test-suite/output/ArgumentsScope.v   | 29 +++++++++++++++++++
 2 files changed, 85 insertions(+)
 create mode 100644 test-suite/output/ArgumentsScope.out
 create mode 100644 test-suite/output/ArgumentsScope.v

(limited to 'test-suite')

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''.
-- 
cgit v1.2.3