From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- test-suite/output/ArgumentsScope.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 test-suite/output/ArgumentsScope.v (limited to 'test-suite/output/ArgumentsScope.v') diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v new file mode 100644 index 00000000..13b5e13d --- /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