From fde8d600c6532f95a03286e58ac68783fe887c68 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Sep 2001 20:54:40 +0000
Subject: Vérification de la syntaxe des options

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2051 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/options.v | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 test-suite/success/options.v

diff --git a/test-suite/success/options.v b/test-suite/success/options.v
new file mode 100644
index 0000000000..9e9af4fa8f
--- /dev/null
+++ b/test-suite/success/options.v
@@ -0,0 +1,34 @@
+(* Check that the syntax for options works *)
+Set Implicit Arguments.
+Unset Implicit Arguments.
+Test Implicit Arguments.
+
+Set Printing Coercions.
+Unset Printing Coercions.
+Test Printing Coercions.
+
+Set Silent.
+Unset Silent.
+Test Silent.
+
+Set Printing Depth 100.
+Print Table Printing Depth.
+
+Parameter i : bool -> nat.
+Coercion i : bool >-> nat.
+Set Printing Coercion i.
+Unset Printing Coercion i.
+Test Printing Coercion i.
+
+Print Table Printing Let.
+Print Table Printing If.
+Remove Printing Let sig.
+Remove Printing If bool.
+
+Unset Printing Synth.
+Set Printing Synth.
+Test Printing Synth.
+
+Unset Printing Wildcard.
+Set Printing Wildcard.
+Test Printing Wildcard.
-- 
cgit v1.2.3