From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 test-suite/output/Arguments.v | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 test-suite/output/Arguments.v

(limited to 'test-suite/output/Arguments.v')

diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
new file mode 100644
index 00000000..3a94f19a
--- /dev/null
+++ b/test-suite/output/Arguments.v
@@ -0,0 +1,40 @@
+Arguments minus n m : simpl nomatch. 
+About minus.
+Arguments minus n / m : simpl nomatch. 
+About minus.
+Arguments minus !n / m : simpl nomatch. 
+About minus.
+Arguments minus !n !m /.
+About minus.
+Arguments minus !n !m.
+About minus.
+Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
+  fun x => (f (fst x), g (snd x)).
+Delimit Scope foo_scope with F.
+Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
+About pf.
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+Arguments fcomp {_ _ _}%type_scope f g x /.
+About fcomp.
+Definition volatile := fun x : nat => x.
+Arguments volatile /.
+About volatile.
+Set Implicit Arguments.
+Section S1.
+Variable T1 : Type.
+Section S2.
+Variable T2 : Type.
+Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
+  match n, m with
+  | 0,_ => 0
+  | S _, 0 => n
+  | S n', S m' => f x y n' v m' end.
+About f.
+Global Arguments f x y !n !v !m.
+About f.
+End S2.
+About f.
+End S1.
+About f.
+Arguments f : clear implicits and scopes.
+About f.
-- 
cgit v1.2.3