aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/options.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-30 08:11:13 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-04-30 08:11:13 +0000
commit1c0b79b69eaf1ff3c773cef08d24761960dcdbeb (patch)
treeaf1766f4b546671832a04f11c55a28159f34740a /test-suite/success/options.v
parent2e93c7e89c4acd51d4f37ccf8c13dcad17b67b0d (diff)
Modification syntaxe de Test
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9816 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/options.v')
-rw-r--r--test-suite/success/options.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/options.v b/test-suite/success/options.v
index bb6781506..f43a46940 100644
--- a/test-suite/success/options.v
+++ b/test-suite/success/options.v
@@ -20,7 +20,7 @@ Parameter i : bool -> nat.
Coercion i : bool >-> nat.
Add Printing Coercion i.
Remove Printing Coercion i.
-Test Printing Coercion i.
+Test Printing Coercion for i.
Test Printing Let.
Test Printing If.