diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 12 | ||||
| -rw-r--r-- | doc/refman/Natural.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 10 | ||||
| -rw-r--r-- | library/goptions.ml | 2 | ||||
| -rw-r--r-- | library/goptions.mli | 1 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 58 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 3 |
7 files changed, 50 insertions, 42 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 110ba8243..0101b1096 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -2102,13 +2102,15 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_set_option(table1) | VernacSetOption (table, v) -> let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in let value = match v with | BoolValue _ -> assert false @@ -2121,7 +2123,8 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_unset_option(table1) | VernacAddOption (table, l) -> let values = @@ -2136,7 +2139,8 @@ let rec xlate_vernac = let table1 = match table with PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s) - | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in + | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) + | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1)) | VernacImport(true, a::l) -> CT_export_id(CT_id_ne_list(reference_to_ct_ID a, diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex index 69dfab87c..9a9abe5df 100644 --- a/doc/refman/Natural.tex +++ b/doc/refman/Natural.tex @@ -121,7 +121,7 @@ declared as implicit, type \comindex{Test Natural} \begin{coq_example*} -Test Natural Implicit lem1. +Test Natural Implicit for lem1. \end{coq_example*} \subsubsection*{Implicit proof constructors} @@ -211,7 +211,7 @@ By default, the data type \verb=nat= and the inductive connectives As above, you can remove or test a constant declared implicit. Use {\tt Remove Natural Contractible $id$} or {\tt Test Natural -Contractible $id$}. +Contractible for $id$}. \asubsection{Contractible proof steps} @@ -328,7 +328,7 @@ a non inductive transparent definition. As for implicit and contractible definitions, you can remove or test a non inductive definition declared transparent. Use \texttt{Remove Natural Transparent} \ident or -\texttt{Test Natural Transparent} \ident. +\texttt{Test Natural Transparent for} \ident. \subsubsection*{Transparent inductive definitions} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 769927caf..f6e44f91a 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -424,7 +424,7 @@ The default is to not print synthesisable types. \subsubsection{Printing matching on irrefutable pattern \comindex{Add Printing Let {\ident}} \comindex{Remove Printing Let {\ident}} -\comindex{Test Printing Let {\ident}} +\comindex{Test Printing Let for {\ident}} \comindex{Print Table Printing Let}} If an inductive type has just one constructor, @@ -443,7 +443,7 @@ pattern-matching is written using a {\tt let} expression. This removes {\ident} from this list. \begin{quote} -{\tt Test Printing Let {\ident}.} +{\tt Test Printing Let for {\ident}.} \end{quote} This tells if {\ident} belongs to the list. @@ -460,7 +460,7 @@ it is sensible to the command {\tt Reset}. \subsubsection{Printing matching on booleans \comindex{Add Printing If {\ident}} \comindex{Remove Printing If {\ident}} -\comindex{Test Printing If {\ident}} +\comindex{Test Printing If for {\ident}} \comindex{Print Table Printing If}} If an inductive type is isomorphic to the boolean type, @@ -479,7 +479,7 @@ pattern-matching is written using an {\tt if} expression. This removes {\ident} from this list. \begin{quote} -{\tt Test Printing If {\ident}.} +{\tt Test Printing If for {\ident}.} \end{quote} This tells if {\ident} belongs to the list. @@ -498,7 +498,7 @@ it is sensible to the command {\tt Reset}. This example emphasizes what the printing options offer. \begin{coq_example} -Test Printing Let prod. +Test Printing Let for prod. Print fst. Remove Printing Let prod. Unset Printing Synth. diff --git a/library/goptions.ml b/library/goptions.ml index 4eb8f2402..4be15569e 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -25,10 +25,12 @@ open Mod_subst type option_name = | PrimaryTable of string | SecondaryTable of string * string + | TertiaryTable of string * string * string let nickname = function | PrimaryTable s -> s | SecondaryTable (s1,s2) -> s1^" "^s2 + | TertiaryTable (s1,s2,s3) -> s1^" "^s2^" "^s3 let error_undeclared_key key = error ((nickname key)^": no table or option of this type") diff --git a/library/goptions.mli b/library/goptions.mli index 4709fc1c8..53f6a6cdb 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -68,6 +68,7 @@ open Mod_subst type option_name = | PrimaryTable of string | SecondaryTable of string * string + | TertiaryTable of string * string * string val error_undeclared_key : option_name -> 'a diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 6d0e3ffc4..ce9aacee8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -551,48 +551,41 @@ GEXTEND Gram VernacAddMLPath (true, dir) (* Pour intervenir sur les tables de paramètres *) - | "Set"; table = IDENT; field = IDENT; v = option_value -> - VernacSetOption (SecondaryTable (table,field),v) - | "Set"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value -> - VernacAddOption (SecondaryTable (table,field),lv) - | "Set"; table = IDENT; field = IDENT -> - VernacSetOption (SecondaryTable (table,field),BoolValue true) - | IDENT "Unset"; table = IDENT; field = IDENT -> - VernacUnsetOption (SecondaryTable (table,field)) - | IDENT "Unset"; table = IDENT; field = IDENT; lv = LIST1 option_ref_value -> - VernacRemoveOption (SecondaryTable (table,field),lv) - | "Set"; table = IDENT; value = option_value -> - VernacSetOption (PrimaryTable table, value) - | "Set"; table = IDENT -> - VernacSetOption (PrimaryTable table, BoolValue true) - | IDENT "Unset"; table = IDENT -> - VernacUnsetOption (PrimaryTable table) - - | IDENT "Print"; IDENT "Table"; table = IDENT; field = IDENT -> - VernacPrintOption (SecondaryTable (table,field)) - | IDENT "Print"; IDENT "Table"; table = IDENT -> - VernacPrintOption (PrimaryTable table) + | "Set"; table = option_table; v = option_value -> + VernacSetOption (table,v) + | "Set"; table = option_table -> + VernacSetOption (table,BoolValue true) + | IDENT "Unset"; table = option_table -> + VernacUnsetOption table + + | IDENT "Print"; IDENT "Table"; table = option_table -> + VernacPrintOption table | 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 *) | 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 = IDENT; field = IDENT; v = LIST1 option_ref_value - -> VernacMemOption (SecondaryTable (table,field), v) - | IDENT "Test"; table = IDENT; field = IDENT -> - VernacPrintOption (SecondaryTable (table,field)) - | IDENT "Test"; table = IDENT; v = LIST1 option_ref_value -> - VernacMemOption (PrimaryTable table, v) - | IDENT "Test"; table = IDENT -> - VernacPrintOption (PrimaryTable table) + | IDENT "Test"; table = option_table; "for"; v = LIST1 option_ref_value + -> VernacMemOption (table, v) + | IDENT "Test"; table = option_table -> + VernacPrintOption table | 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 ]] ; @@ -657,6 +650,11 @@ GEXTEND Gram [ [ id = global -> QualidRefValue id | 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 ] ] + ; as_dirpath: [ [ d = OPT [ "as"; d = dirpath -> d ] -> d ] ] ; diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 9b0186368..e9d960e37 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -162,6 +162,9 @@ let pr_option_ref_value = function 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_set_option a b = let pr_opt_value = function |