diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-01 21:59:00 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-01 21:59:00 +0000 |
commit | 7f110df7d7ff6a4d43f3c8d19305b20e24f4800e (patch) | |
tree | 506315cd644fe671eebea691941bdcb8baaa171b /test-suite/output | |
parent | f6007680bfa822ecc3d2f101fb6e21e2b1464b1b (diff) |
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
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/ArgumentsScope.out | 56 | ||||
-rw-r--r-- | test-suite/output/ArgumentsScope.v | 29 |
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 000000000..6643c1429 --- /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 000000000..13b5e13dd --- /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''. |