diff options
| author | herbelin | 2009-08-02 19:51:48 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-02 19:51:48 +0000 |
| commit | 25dde2366a4db47e5da13b2bbe4d03a31235706f (patch) | |
| tree | 5fe442297f6aabf515ce4aad817e31818fb4deb0 /parsing | |
| parent | 581223c7fc607b5121013928fd83606b82ea8531 (diff) | |
Improved parameterization of Coq:
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 16 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 9 |
2 files changed, 10 insertions, 15 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 387ee2b030..41ac3b5104 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -647,13 +647,13 @@ GEXTEND Gram VernacPrintOption table | IDENT "Add"; table = IDENT; field = IDENT; v = LIST1 option_ref_value - -> VernacAddOption (SecondaryTable (table,field), v) + -> VernacAddOption ([table;field], v) (* Un value global ci-dessous va être caché par un field au dessus! *) (* 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) + VernacAddOption ([table], v) | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value -> VernacMemOption (table, v) @@ -661,9 +661,9 @@ GEXTEND Gram VernacPrintOption table | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value - -> VernacRemoveOption (SecondaryTable (table,field), v) + -> VernacRemoveOption ([table;field], v) | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> - VernacRemoveOption (PrimaryTable table, v) + VernacRemoveOption ([table], v) | IDENT "proof" -> VernacDeclProof | "return" -> VernacReturn ]] @@ -735,9 +735,7 @@ GEXTEND Gram | s = STRING -> StringRefValue s ] ] ; option_table: - [ [ f1 = IDENT; f2 = IDENT; f3 = IDENT -> TertiaryTable (f1,f2,f3) - | f1 = IDENT; f2 = IDENT -> SecondaryTable (f1,f2) - | f1 = IDENT -> PrimaryTable f1 ] ] + [ [ fl = LIST1 IDENT -> fl ]] ; as_dirpath: [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] @@ -781,10 +779,10 @@ GEXTEND Gram (* Tactic Debugger *) | IDENT "Debug"; IDENT "On" -> - VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue true) + VernacSetOption (["Ltac";"Debug"], BoolValue true) | IDENT "Debug"; IDENT "Off" -> - VernacSetOption (SecondaryTable ("Ltac","Debug"), BoolValue false) + VernacSetOption (["Ltac";"Debug"], BoolValue false) ] ]; END diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index be04f584d9..049a227eb0 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -166,12 +166,9 @@ let pr_option_ref_value = function | QualidRefValue id -> pr_reference id | StringRefValue s -> qs s -let pr_printoption a b = match a with - | Goptions.PrimaryTable table -> str table ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b - | Goptions.SecondaryTable (table,field) -> str table ++ spc() ++ str field ++ pr_opt (prlist_with_sep sep pr_option_ref_value) b - | Goptions.TertiaryTable (table,field1,field2) -> str table ++ spc() ++ - str field1 ++ spc() ++ str field2 ++ - pr_opt (prlist_with_sep sep pr_option_ref_value) b +let pr_printoption table b = + prlist_with_sep spc str table ++ + pr_opt (prlist_with_sep sep pr_option_ref_value) b let pr_set_option a b = let pr_opt_value = function |