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

1 files changed, 34 insertions, 0 deletions

diff --git a/test-suite/success/options.v b/test-suite/success/options.v
new file mode 100644
index 000000000..9e9af4fa8
--- /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.