diff options
| author | herbelin | 2007-04-29 10:04:07 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-29 10:04:07 +0000 |
| commit | ac8b30a9d072b7f4b6803ec7283d2661f0d45505 (patch) | |
| tree | e3f37d702cd931d77397b9abd4fee32cbd73fc4e | |
| parent | fb7851ec9be42e9d3b77c9f7034c3995f68b2ced (diff) | |
Suite commit 9810
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9811 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 12 |
2 files changed, 8 insertions, 9 deletions
@@ -41,6 +41,11 @@ Tactics - New tactics "eapply in", "erewrite", "erewrite in". - Unfoldable references can be given by notation rather than by name in unfold. +Miscellaneous + +- Syntax of "Test Printing Let ref" and "Test Printing If ref" changed into + "Test Printing Let for ref" and "Test Printing If for ref". + Changes from V8.1gamma to V8.1 ============================== diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ce9aacee81..f816001578 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -564,12 +564,11 @@ GEXTEND Gram | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value -> VernacAddOption (SecondaryTable (table,field), v) (* Un value global ci-dessous va être caché par un field au dessus! *) - (* Dans la pratique, on a donné priorité aux tables secondaires *) + (* En fait, on donne priorité aux tables secondaires *) + (* Pas de syntaxe pour les tables tertiaires pour cause de conflit *) + (* (mais de toutes façons, pas utilisées) *) | IDENT "Add"; table = IDENT; v = LIST1 option_ref_value -> VernacAddOption (PrimaryTable table, v) - | IDENT "Add"; table = IDENT; field = IDENT; field2 = IDENT; - v = LIST1 option_ref_value - -> VernacAddOption (TertiaryTable (table,field,field2), v) | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value -> VernacMemOption (table, v) @@ -578,13 +577,8 @@ GEXTEND Gram | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value -> VernacRemoveOption (SecondaryTable (table,field), v) - (* Un value global ci-dessous va être caché par un field au dessus! *) - (* Dans la pratique, on a donné priorité aux tables secondaires *) | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> VernacRemoveOption (PrimaryTable table, v) - | IDENT "Remove"; table = IDENT; field = IDENT; field2 = IDENT; - v = LIST1 option_ref_value -> - VernacRemoveOption (TertiaryTable (table,field,field2), v) | IDENT "proof" -> VernacDeclProof | "return" -> VernacReturn ]] |