diff options
35 files changed, 264 insertions, 278 deletions
diff --git a/.gitignore b/.gitignore index 948cd98d7..22f01e7c1 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,27 @@ *.idx *.ilg *.toc +*.atoc +*.comidx +*.comind +*.erridx +*.errind +*.haux +*.hcomind +*.herrind +*.hind +*.htacind +*.htoc +*.ind +*.lof +*.tacidx +*.tacind +*.v.tex +*.v.pdf +*.v.ps +*.v.html +revision +TAGS bin/ config/Makefile config/coq_config.ml @@ -5,22 +5,25 @@ Tactics - Tactic "discriminate" now performs intros before trying to discriminate an hypothesis of the goal (previously it applied intro only if the goal - had the form t1<>t2). + had the form t1<>t2) (exceptional source of incompatibilities - former + behavior can be obtained by "Unset Discriminate Introduction"). - Tactic "rewrite" now supports rewriting on ad hoc equalities such as eq_true. -- Tactic "intuition" now preserves inner "iff" (exceptional source of - incompatibilities solvable by redefining "intuition" as - "unfold iff in *; intuition". +- Tactic "intuition" now preserves inner "iff" and "not" (exceptional + source of incompatibilities solvable by redefining "intuition" as + "unfold iff, not in *; intuition", or by using "Set Intuition Unfolding".) - Improved support of dependent goals over objects in dependent types for "destruct" (rare source of incompatibility). - Tactic "quote" now supports quotation of arbitrary terms (not just the goal). -- Tactic "idtac" now displays its list arguments. +- Tactic "idtac" now displays its "list" arguments. - Tactic "tauto" now proves classical tautologies as soon as classical logic (i.e. library Classical_Prop or Classical) is loaded. - New "Hint Resolve ->" (or "<-") for declaring iff's as oriented hints (wish #2104). - New introduction patterns "*" for introducing the next block of dependent variables and "**" for introducing all quantified variables and hypotheses. +- Pattern Unification for existential variables activated in tactics and + new option "Unset Tactic Evars Pattern Unification" to deactivate it. Tactic Language @@ -38,6 +41,8 @@ Tools - New coqtop/coqc option -beautify to reformat .v files (usable e.g. to globally update notations). - New tool beautify-archive to beautify a full archive of developments. +- New coqtop/coqc option -compat X.Y to simulate the general behavior + of previous versions of Coq (provides e.g. support for 8.2 compatibility). Library diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f60fb222d..e3addd6f0 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -31,7 +31,7 @@ open Genarg let _ = Constrextern.print_evar_arguments := true -let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false +let _ = set_bool_option_value ["Printing";"Matching"] false let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found) (* std_ppcmds *) diff --git a/doc/refman/csdp.cache b/doc/refman/csdp.cache deleted file mode 100644 index 61082f7b8..000000000 --- a/doc/refman/csdp.cache +++ /dev/null @@ -1,120 +0,0 @@ -*** REQUEST *** -"" -2 -3 -2 1 1 -0.10485760000000000000e7 0.10485760000000000000e7 -0 1 1 1 0.10485760000000000000e7 -1 1 2 2 0.10485760000000000000e7 -1 2 1 1 0.10485760000000000000e7 -2 1 1 1 0.10485760000000000000e7 -2 1 1 2 -0.52428800000000000000e6 -2 3 1 1 0.10485760000000000000e7 -*** ANSWER *** -1.170818692744000744e+00 1.447215295915970978e+00 -1 1 1 1 4.689392261611652211e+05 -1 1 1 2 -7.587576130651925923e+05 -1 1 2 2 1.227692381593513535e+06 -1 2 1 1 1.227692381593513535e+06 -1 3 1 1 1.517515226161165396e+06 -2 1 1 1 2.618033982848464447e+00 -2 1 1 2 1.618033984214826360e+00 -2 1 2 2 9.999999983112128898e-01 -2 2 1 1 1.688748897052140516e-09 -2 3 1 1 1.366359508118386529e-09 -*** END *** -*** REQUEST *** -"" -1 -3 -1 1 1 -0.0 -0 1 1 1 0.10485760000000000000e7 -1 2 1 1 -0.10485760000000000000e7 -1 3 1 1 0.10485760000000000000e7 -*** ANSWER *** -Infeasible -*** END *** -*** REQUEST *** -"" -5 -6 -2 1 1 1 1 1 --0.52428800000000000000e6 0.10485760000000000000e7 0.0 0.15728640000000000000e7 0.15728640000000000000e7 -0 1 1 2 0.10485760000000000000e7 -0 4 1 1 0.10485760000000000000e7 -0 6 1 1 0.10485760000000000000e7 -1 1 1 1 0.10485760000000000000e7 -1 1 1 2 -0.10485760000000000000e7 -1 4 1 1 -0.10485760000000000000e7 -1 6 1 1 -0.10485760000000000000e7 -2 1 2 2 0.10485760000000000000e7 -2 4 1 1 0.10485760000000000000e7 -3 2 1 1 0.10485760000000000000e7 -3 4 1 1 -0.10485760000000000000e7 -4 1 1 2 0.52428800000000000000e6 -4 3 1 1 0.10485760000000000000e7 -4 4 1 1 0.10485760000000000000e7 -4 6 1 1 0.10485760000000000000e7 -5 1 1 2 0.52428800000000000000e6 -5 4 1 1 0.10485760000000000000e7 -5 5 1 1 0.10485760000000000000e7 -5 6 1 1 0.10485760000000000000e7 -*** ANSWER *** -3.447076640086706701e-09 1.219413182975184255e-08 4.999999990735581878e-01 9.999999944008177710e-01 9.999999949992444126e-01 -1 1 1 1 6.114634782269312563e-03 -1 1 1 2 -9.171942037320746088e-03 -1 1 2 2 1.528658692482759429e-02 -1 2 1 1 5.242880015286683338e+05 -1 3 1 1 1.048575996628944878e+06 -1 4 1 1 5.242880015286696143e+05 -1 5 1 1 1.048575997256440693e+06 -1 6 1 1 1.048575987770750769e+06 -2 1 1 1 2.499999992691011474e+00 -2 1 1 2 1.499999994152806382e+00 -2 1 2 2 9.999999970764240631e-01 -2 2 1 1 2.923578058235802830e-09 -2 3 1 1 1.461800604315761330e-09 -2 4 1 1 2.923578058235802830e-09 -2 5 1 1 1.461800574968901974e-09 -2 6 1 1 1.461818077871661339e-09 -*** END *** -*** REQUEST *** -"" -2 -3 -2 1 1 -0.10485760000000000000e7 0.10485760000000000000e7 -0 1 1 2 0.52428800000000000000e6 -0 2 1 1 -0.10485760000000000000e7 -1 1 1 1 0.10485760000000000000e7 -1 1 1 2 -0.52428800000000000000e6 -1 2 1 1 0.10485760000000000000e7 -2 1 2 2 0.10485760000000000000e7 -2 3 1 1 0.10485760000000000000e7 -*** ANSWER *** -4.472193867846282478e-01 1.170814599989497884e+00 -1 1 1 1 4.689435163452157285e+05 -1 1 1 2 -7.587597578585391166e+05 -1 1 2 2 1.227688090626724996e+06 -1 2 1 1 1.517519516345215729e+06 -1 3 1 1 1.227688090626724996e+06 -2 1 1 1 2.618033965193043766e+00 -2 1 1 2 1.618033970702413393e+00 -2 1 2 2 9.999999931920802165e-01 -2 2 1 1 5.509546873900648946e-09 -2 3 1 1 6.807899670209652660e-09 -*** END *** -*** REQUEST *** -"" -0 -1 -4 -0.10000000000000000000e1 0.10000000000000000000e1 0.10000000000000000000e1 0.10000000000000000000e1 -0 1 1 1 -0.10000000000000000000e1 -0 1 2 2 -0.20000000000000000000e1 -0 1 3 3 0.10000000000000000000e1 -0 1 4 4 0.20000000000000000000e1 -*** ANSWER *** -Failure -*** END *** diff --git a/ide/coq.ml b/ide/coq.ml index 5572dd8ae..d81bb42f2 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -156,10 +156,7 @@ let prepare_option (l,dft) = let unset = (String.concat " " ("Unset"::l)) ^ "." in if dft then unset,set else set,unset -let coqide_known_option = function - | Goptions.TertiaryTable (a,b,c) -> List.mem [a;b;c] !known_options - | Goptions.SecondaryTable (a,b) -> List.mem [a;b] !known_options - | Goptions.PrimaryTable a -> List.mem [a] !known_options +let coqide_known_option table = List.mem table !known_options let with_printing_implicit = prepare_option printing_implicit_data let with_printing_coercions = prepare_option printing_coercions_data @@ -278,8 +275,7 @@ let rec attribute_of_vernac_command = function | VernacDeclareImplicits _ -> [] | VernacReserve _ -> [] | VernacSetOpacity _ -> [] - | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) -> - [DebugCommand] + | VernacSetOption (["Ltac";"Debug"], _) -> [DebugCommand] | VernacSetOption (o,BoolValue true) | VernacUnsetOption o -> if coqide_known_option o then [KnownOptionCommand] else [] | VernacSetOption _ -> [] diff --git a/library/goptions.ml b/library/goptions.ml index b5a8b00ea..95259c9b5 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -22,15 +22,9 @@ open Mod_subst (****************************************************************************) (* 0- Common things *) -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 +type option_name = string list + +let nickname table = String.concat " " table 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 53f6a6cdb..aefddbbda 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -15,11 +15,12 @@ - Variables storing options value are created by applying one of the [declare_int_option], [declare_bool_option], ... functions. - Each table/option is uniquely identified by a key of type [option_name]. - There are two kinds of table/option idenfiers: the primary ones - (supposed to be more global) and the secondary ones + Each table/option is uniquely identified by a key of type [option_name] + which consists in a list of strings. Note that for parsing constraints, + table names must not be made of more than 2 strings while option names + can be of arbitrary length. - The declaration of a table, say of name [SecondaryTable("Toto","Titi")] + The declaration of a table, say of name [["Toto";"Titi"]] automatically makes available the following vernacular commands: Add Toto Titi foo. @@ -28,26 +29,18 @@ Test Toto Titi. The declaration of a non boolean option value, say of name - [SecondaryTable("Tata","Tutu")], automatically makes available the + [["Tata";"Tutu";"Titi"]], automatically makes available the following vernacular commands: - Set Tata Tutu val. - Print Table Tata Tutu. + Set Tata Tutu Titi val. + Print Table Tata Tutu Titi. If it is the declaration of a boolean value, the following vernacular commands are made available: - Set Tata Tutu. - Unset Tata Tutu. - Print Table Tata Tutu. (* synonym: Test Table Tata Tutu. *) - - For a primary table, say of name [PrimaryTable("Bidule")], the - vernacular commands look like - - Add Bidule foo. - Print Table Bidule foo. - Set Bidule foo. - ... + Set Tata Tutu Titi. + Unset Tata Tutu Titi. + Print Table Tata Tutu Titi. (* synonym: Test Table Tata Tutu Titi. *) The created table/option may be declared synchronous or not (synchronous = consistent with the resetting commands) *) @@ -64,11 +57,8 @@ open Mod_subst (*s Things common to tables and options. *) -(* The type of primary or secondary table/option keys *) -type option_name = - | PrimaryTable of string - | SecondaryTable of string * string - | TertiaryTable of string * string * string +(* The type of table/option keys *) +type option_name = string list val error_undeclared_key : option_name -> 'a diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 387ee2b03..41ac3b510 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 be04f584d..049a227eb 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 diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 2d7dd9d6c..418980c54 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -31,7 +31,7 @@ let _= let gdopt= { optsync=true; optname="Congruence Verbose"; - optkey=SecondaryTable("Congruence","Verbose"); + optkey=["Congruence";"Verbose"]; optread=(fun ()-> !cc_verbose); optwrite=(fun b -> cc_verbose := b)} in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f1e8f42fe..83a780198 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -327,7 +327,7 @@ let auto_inline () = !auto_inline_ref let _ = declare_bool_option {optsync = true; optname = "Extraction AutoInline"; - optkey = SecondaryTable ("Extraction", "AutoInline"); + optkey = ["Extraction"; "AutoInline"]; optread = auto_inline; optwrite = (:=) auto_inline_ref} @@ -340,7 +340,7 @@ let type_expand () = !type_expand_ref let _ = declare_bool_option {optsync = true; optname = "Extraction TypeExpand"; - optkey = SecondaryTable ("Extraction", "TypeExpand"); + optkey = ["Extraction"; "TypeExpand"]; optread = type_expand; optwrite = (:=) type_expand_ref} @@ -389,14 +389,14 @@ let optims () = !opt_flag_ref let _ = declare_bool_option {optsync = true; optname = "Extraction Optimize"; - optkey = SecondaryTable ("Extraction", "Optimize"); + optkey = ["Extraction"; "Optimize"]; optread = (fun () -> !int_flag_ref <> 0); optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} let _ = declare_int_option { optsync = true; optname = "Extraction Flag"; - optkey = SecondaryTable("Extraction","Flag"); + optkey = ["Extraction";"Flag"]; optread = (fun _ -> Some !int_flag_ref); optwrite = (function | None -> chg_flag 0 diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index d7c5b66ae..96c5bcae4 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -30,7 +30,7 @@ let _= let gdopt= { optsync=true; optname="Firstorder Depth"; - optkey=SecondaryTable("Firstorder","Depth"); + optkey=["Firstorder";"Depth"]; optread=(fun ()->Some !ground_depth); optwrite= (function @@ -45,7 +45,7 @@ let _= let gdopt= { optsync=true; optname="Congruence Depth"; - optkey=SecondaryTable("Congruence","Depth"); + optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); optwrite= (function diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 69cc0607b..b29bdf3f1 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -495,7 +495,7 @@ let function_debug_sig = { optsync = false; optname = "Function debug"; - optkey = PrimaryTable("Function_debug"); + optkey = ["Function_debug"]; optread = (fun () -> !function_debug); optwrite = (fun b -> function_debug := b) } @@ -514,7 +514,7 @@ let strict_tcc_sig = { optsync = false; optname = "Raw Function Tcc"; - optkey = PrimaryTable("Function_raw_tcc"); + optkey = ["Function_raw_tcc"]; optread = (fun () -> !strict_tcc); optwrite = (fun b -> strict_tcc := b) } diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index 6f9e673a9..bff8cae26 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -404,7 +404,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function | CPrim (_, String _) -> xlate_error "CPrim (String): TODO" | CHole _ -> CT_existvarc (* I assume CDynamic has been inserted to make free form extension of - the language possible, but this would go agains the logic of pcoq anyway. *) + the language possible, but this would go against the logic of pcoq anyway. *) | CDynamic (_, _) -> assert false | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula num) @@ -2179,21 +2179,21 @@ let rec xlate_vernac = | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s) | VernacTime(v) -> CT_time(xlate_vernac v) | VernacTimeout(n,v) -> CT_timeout(CT_int n,xlate_vernac v) - | VernacSetOption (Goptions.SecondaryTable ("Implicit", "Arguments"), BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[]) + | VernacSetOption (["Implicit"; "Arguments"], BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[]) |VernacExactProof f -> CT_proof(xlate_formula f) | VernacSetOption (table, BoolValue true) -> 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) - | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in + [s] -> CT_coerce_ID_to_TABLE(CT_ident s) + | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2) + | _ -> xlate_error "TODO: arbitrary-length Table names" 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) - | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in + [s] -> CT_coerce_ID_to_TABLE(CT_ident s) + | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2) + | _ -> xlate_error "TODO: arbitrary-length Table names" in let value = match v with | BoolValue _ -> assert false @@ -2205,9 +2205,9 @@ let rec xlate_vernac = | VernacUnsetOption(table) -> 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) - | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in + [s] -> CT_coerce_ID_to_TABLE(CT_ident s) + | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2) + | _ -> xlate_error "TODO: arbitrary-length Table names" in CT_unset_option(table1) | VernacAddOption (table, l) -> let values = @@ -2221,9 +2221,9 @@ let rec xlate_vernac = match values with [] -> assert false | a::b -> (a,b) in 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) - | TertiaryTable(s1,s2,s3) -> xlate_error "TODO: TertiaryTable" in + [s] -> CT_coerce_ID_to_TABLE(CT_ident s) + | [s1;s2] -> CT_table(CT_ident s1, CT_ident s2) + | _ -> xlate_error "TODO: arbitrary-length Table names" 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/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 535459885..8c8640ea5 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -61,7 +61,7 @@ let _ = declare_bool_option { optsync = false; optname = "Omega system time displaying flag"; - optkey = SecondaryTable ("Omega","System"); + optkey = ["Omega";"System"]; optread = read display_system_flag; optwrite = write display_system_flag } @@ -69,7 +69,7 @@ let _ = declare_bool_option { optsync = false; optname = "Omega action display flag"; - optkey = SecondaryTable ("Omega","Action"); + optkey = ["Omega";"Action"]; optread = read display_action_flag; optwrite = write display_action_flag } @@ -77,7 +77,7 @@ let _ = declare_bool_option { optsync = false; optname = "Omega old style flag"; - optkey = SecondaryTable ("Omega","OldStyle"); + optkey = ["Omega";"OldStyle"]; optread = read old_style_flag; optwrite = write old_style_flag } diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 9d9d66bb2..1fee72a60 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -50,7 +50,7 @@ let pruning = ref true let opt_pruning= {optsync=true; optname="Rtauto Pruning"; - optkey=SecondaryTable("Rtauto","Pruning"); + optkey=["Rtauto";"Pruning"]; optread=(fun () -> !pruning); optwrite=(fun b -> pruning:=b)} diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 6cde1ddcf..b47bbaa93 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -245,7 +245,7 @@ let verbose = ref false let opt_verbose= {optsync=true; optname="Rtauto Verbose"; - optkey=SecondaryTable("Rtauto","Verbose"); + optkey=["Rtauto";"Verbose"]; optread=(fun () -> !verbose); optwrite=(fun b -> verbose:=b)} @@ -256,7 +256,7 @@ let check = ref false let opt_check= {optsync=true; optname="Rtauto Check"; - optkey=SecondaryTable("Rtauto","Check"); + optkey=["Rtauto";"Check"]; optread=(fun () -> !check); optwrite=(fun b -> check:=b)} diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index a54b3a86f..a8f5815bc 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -77,7 +77,7 @@ let _ = declare_bool_option { optsync = true; optname = "transparency of Program obligations"; - optkey = (SecondaryTable ("Transparent","Obligations")); + optkey = ["Transparent";"Obligations"]; optread = get_proofs_transparency; optwrite = set_proofs_transparency; } diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 11d6ed093..911ded641 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -413,7 +413,7 @@ module CoercionPrinting = let encode = coercion_of_reference let subst = subst_coe_typ let printer x = pr_global_env Idset.empty x - let key = Goptions.SecondaryTable ("Printing","Coercion") + let key = ["Printing";"Coercion"] let title = "Explicitly printed coercions: " let member_message x b = str "Explicit printing of coercion " ++ printer x ++ diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b2e9f0e6b..d43bc0780 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -74,7 +74,7 @@ module PrintingCasesMake = if kn' == kn then obj else (kn',i), ints let printer (ind,_) = pr_global_env Idset.empty (IndRef ind) - let key = Goptions.SecondaryTable ("Printing",Test.field) + let key = ["Printing";Test.field] let title = Test.title let member_message x = Test.member_message (printer x) let synchronous = true @@ -118,7 +118,7 @@ let force_wildcard () = !wildcard_value let _ = declare_bool_option { optsync = true; optname = "forced wildcard"; - optkey = SecondaryTable ("Printing","Wildcard"); + optkey = ["Printing";"Wildcard"]; optread = force_wildcard; optwrite = (:=) wildcard_value } @@ -128,7 +128,7 @@ let synthetize_type () = !synth_type_value let _ = declare_bool_option { optsync = true; optname = "pattern matching return type synthesizability"; - optkey = SecondaryTable ("Printing","Synth"); + optkey = ["Printing";"Synth"]; optread = synthetize_type; optwrite = (:=) synth_type_value } @@ -138,7 +138,7 @@ let reverse_matching () = !reverse_matching_value let _ = declare_bool_option { optsync = true; optname = "pattern-matching reversibility"; - optkey = SecondaryTable ("Printing","Matching"); + optkey = ["Printing";"Matching"]; optread = reverse_matching; optwrite = (:=) reverse_matching_value } diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 14121d328..45fbe3227 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -330,7 +330,7 @@ let is_predicate_explicitly_dep env pred arsign = srec (push_rel_assum (na,t) env) b arsign | Lambda (na,_,_), _ -> - (* The following code has impact on the introduction names + (* The following code has an impact on the introduction names given by the tactics "case" and "inversion": when the elimination is not dependent, "case" uses Anonymous for inductive types in Prop and names created by mkProd_name for diff --git a/pretyping/unification.ml b/pretyping/unification.ml index dcb5efae5..d48c002e2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -122,6 +122,18 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) +(* Option introduced and activated in Coq 8.3 *) +let global_evars_pattern_unification_flag = ref true + +open Goptions +let _ = + declare_bool_option + { optsync = true; + optname = "pattern-unification for existential variables in tactics"; + optkey = ["Tactic";"Evars";"Pattern";"Unification"]; + optread = (fun () -> !global_evars_pattern_unification_flag); + optwrite = (:=) global_evars_pattern_unification_flag } + type unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; use_metas_eagerly : bool; @@ -146,6 +158,9 @@ let default_no_delta_unify_flags = { use_evars_pattern_unification = true; } +let use_evars_pattern_unification flags = + !global_evars_pattern_unification_flag && flags.use_evars_pattern_unification + let expand_key env = function | Some (ConstKey cst) -> constant_opt_value env cst | Some (VarKey id) -> named_body id env @@ -231,13 +246,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2 | App (f1,l1), _ when - (isMeta f1 || flags.use_evars_pattern_unification && isEvar f1) & + (isMeta f1 || use_evars_pattern_unification flags && isEvar f1) & is_unification_pattern curenvnb f1 l1 cN & not (dependent f1 cN) -> solve_pattern_eqn_array curenvnb f1 l1 cN substn | _, App (f2,l2) when - (isMeta f2 || flags.use_evars_pattern_unification && isEvar f2) & + (isMeta f2 || use_evars_pattern_unification flags && isEvar f2) & is_unification_pattern curenvnb f2 l2 cM & not (dependent f2 cM) -> solve_pattern_eqn_array curenvnb f2 l2 cM substn diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 2d3fea3fd..64a3dcf91 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -129,7 +129,7 @@ let parse_args () = | ("-I"|"-include"|"-outputstate" |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object"|"-user" - |"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem -> + |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem -> begin match rem with | s :: rem' -> parse (cfiles,s::o::args) rem' diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index e909a1f4f..515b184da 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -44,7 +44,7 @@ let _ = declare_bool_option { optsync = true; optname = "strict mode"; - optkey = (SecondaryTable ("Strict","Proofs")); + optkey = ["Strict";"Proofs"]; optread = get_strictness; optwrite = set_strictness } diff --git a/tactics/equality.ml b/tactics/equality.ml index 3cf5cfd73..ce0677cae 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -44,6 +44,19 @@ open Clenv open Clenvtac open Evd +(* Options *) + +let discr_do_intro = ref true + +open Goptions +let _ = + declare_bool_option + { optsync = true; + optname = "automatic introduction of hypotheses by discriminate"; + optkey = ["Discriminate";"Introduction"]; + optread = (fun () -> !discr_do_intro); + optwrite = (:=) discr_do_intro } + (* Rewriting tactics *) type orientation = bool @@ -676,10 +689,13 @@ let discrClause with_evars = onClause (discrSimpleClause with_evars) let discrEverywhere with_evars = tclORELSE - (tclTHEN - (tclREPEAT introf) - (Tacticals.tryAllHyps - (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) + (if !discr_do_intro then + (tclTHEN + (tclREPEAT introf) + (Tacticals.tryAllHyps + (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) + else (* <= 8.2 compat *) + Tacticals.tryAllHypsAndConcl (discrSimpleClause with_evars)) (fun gls -> errorlabstrm "DiscrEverywhere" (str"No discriminable equalities.")) diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 099d60c09..bbc1285e2 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -45,6 +45,17 @@ let strict_in_hyp_and_ccl = false (* Whether unit type includes equality types *) let strict_unit = false +(* Whether inner iff are unfolded *) +let iff_unfolding = ref false + +open Goptions +let _ = + declare_bool_option + { optsync = true; + optname = "unfolding of iff and not in intuition"; + optkey = ["Intuition";"Iff";"Unfolding"]; + optread = (fun () -> !iff_unfolding); + optwrite = (:=) iff_unfolding } (** Test *) @@ -180,6 +191,7 @@ let simplif ist = (match reverse goal with | id: ?X1 |- _ => $t_is_conj; elim id; do 2 intro; clear id | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.not _) |- _ => red in id | id: ?X1 |- _ => $t_is_disj; elim id; intro; clear id | id0: ?X1 -> ?X2, id1: ?X1|- _ => (* generalize (id0 id1); intro; clear id0 does not work @@ -204,6 +216,7 @@ let simplif ist = (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *) | |- ?X1 => $t_is_conj; split | |- (Coq.Init.Logic.iff _ _) => split + | |- (Coq.Init.Logic.not _) => red end; $t_not_dep_intros) >> @@ -236,7 +249,10 @@ let rec tauto_intuit t_reduce solver ist = ) >> let reduction_not _ist = - <:tactic< unfold Coq.Init.Logic.not in * >> + if !iff_unfolding then + <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >> + else + <:tactic< unfold Coq.Init.Logic.not in * >> let t_reduction_not = tacticIn reduction_not diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 520f9b631..29bef7b5a 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -310,7 +310,7 @@ let end_autoinstance () = let _ = Goptions.declare_bool_option { Goptions.optsync=true; - Goptions.optkey=Goptions.PrimaryTable("Autoinstance"); + Goptions.optkey=["Autoinstance"]; Goptions.optname="automatic typeclass instance recognition"; Goptions.optread=(fun () -> !autoinstance_opt); Goptions.optwrite=(fun b -> if b then begin_autoinstance() else end_autoinstance()) } diff --git a/toplevel/command.ml b/toplevel/command.ml index 7d615028e..48a5119d1 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -272,7 +272,7 @@ let _ = declare_bool_option { optsync = true; optname = "automatic declaration of boolean equality"; - optkey = (SecondaryTable ("Equality","Scheme")); + optkey = ["Equality";"Scheme"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } @@ -640,7 +640,7 @@ let _ = declare_bool_option { optsync = true; optname = "automatic declaration of eliminations"; - optkey = (SecondaryTable ("Elimination","Schemes")); + optkey = ["Elimination";"Schemes"]; optread = (fun () -> !elim_flag) ; optwrite = (fun b -> elim_flag := b) } diff --git a/toplevel/coqcompat.ml b/toplevel/coqcompat.ml new file mode 100644 index 000000000..8bf1e9bd0 --- /dev/null +++ b/toplevel/coqcompat.ml @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* File initially created by Hugo Herbelin, Aug 2009 *) + +(* This file centralizes the support for compatibility with previous + versions of Coq *) + +open Pp +open Util +open Goptions + +let set_compat_options = function + | "8.2" -> + set_bool_option_value ["Tactic";"Evars";"Pattern";"Unification"] false; + set_bool_option_value ["Discriminate";"Introduction"] false; + set_bool_option_value ["Intuition";"Iff";"Unfolding"] true + + | "8.1" -> + warning "Compatibility with versions 8.1 not supported." + + | "8.0" -> + warning "Compatibility with versions 8.0 not supported." + + | s -> + error ("Unknown compatibility version \""^s^"\".") diff --git a/toplevel/coqcompat.mli b/toplevel/coqcompat.mli new file mode 100644 index 000000000..59b249829 --- /dev/null +++ b/toplevel/coqcompat.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +val set_compat_options : string -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 696ce1282..a699e528b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -163,6 +163,12 @@ let set_vm_opt () = Flags.set_boxed_definitions !boxed_def; Vconv.set_use_vm !use_vm +(*s Compatibility options *) + +let compat_version = ref None +let set_compat_options () = + Option.iter Coqcompat.set_compat_options !compat_version + (*s Parsing of the command line. We no longer use [Arg.parse], in order to use share [Usage.print_usage] between coqtop and coqc. *) @@ -267,6 +273,9 @@ let parse_args is_ide = | "-debug" :: rem -> set_debug (); parse rem + | "-compat" :: v :: rem -> compat_version := Some v; parse rem + | "-compat" :: [] -> usage () + | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem | "-emacs-U" :: rem -> Flags.print_emacs := true; @@ -293,7 +302,9 @@ let parse_args is_ide = | "-user" :: u :: rem -> set_rcuser u; parse rem | "-user" :: [] -> usage () - | "-notactics" :: rem -> remove_top_ml (); parse rem + | "-notactics" :: rem -> + warning "Obsolete option \"-notactics\"."; + remove_top_ml (); parse rem | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem @@ -339,6 +350,7 @@ let init is_ide = init_load_path (); inputstate (); set_vm_opt (); + set_compat_options (); engage (); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index 13b27d5ab..7f759cad9 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -21,4 +21,5 @@ Protectedtoplevel Toplevel Usage Coqinit +Coqcompat Coqtop diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 8a8480c41..fcb14b2c6 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -33,6 +33,7 @@ let print_usage_channel co command = -is f (idem) -nois start with an empty state -outputstate f write state in file f.coq + -compat X.Y provides compatibility support for Coq version X.Y -load-ml-object f load ML object file f -load-ml-source f load ML file f diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 5d76f4ff2..fa56e60f6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -785,7 +785,7 @@ let _ = declare_bool_option { optsync = false; optname = "silent"; - optkey = (PrimaryTable "Silent"); + optkey = ["Silent"]; optread = is_silent; optwrite = make_silent_if_not_pcoq } @@ -793,7 +793,7 @@ let _ = declare_bool_option { optsync = true; optname = "implicit arguments"; - optkey = (SecondaryTable ("Implicit","Arguments")); + optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } @@ -801,7 +801,7 @@ let _ = declare_bool_option { optsync = true; optname = "strict implicit arguments"; - optkey = (SecondaryTable ("Strict","Implicit")); + optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } @@ -809,7 +809,7 @@ let _ = declare_bool_option { optsync = true; optname = "strong strict implicit arguments"; - optkey = (TertiaryTable ("Strongly","Strict","Implicit")); + optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; optwrite = Impargs.make_strongly_strict_implicit_args } @@ -817,7 +817,7 @@ let _ = declare_bool_option { optsync = true; optname = "contextual implicit arguments"; - optkey = (SecondaryTable ("Contextual","Implicit")); + optkey = ["Contextual";"Implicit"]; optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } @@ -825,7 +825,7 @@ let _ = (* declare_bool_option *) (* { optsync = true; *) (* optname = "forceable implicit arguments"; *) -(* optkey = (SecondaryTable ("Forceable","Implicit")); *) +(* optkey = ["Forceable";"Implicit")); *) (* optread = Impargs.is_forceable_implicit_args; *) (* optwrite = Impargs.make_forceable_implicit_args } *) @@ -833,7 +833,7 @@ let _ = declare_bool_option { optsync = true; optname = "implicit status of reversible patterns"; - optkey = (TertiaryTable ("Reversible","Pattern","Implicit")); + optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; optwrite = Impargs.make_reversible_pattern_implicit_args } @@ -841,7 +841,7 @@ let _ = declare_bool_option { optsync = true; optname = "maximal insertion of implicit"; - optkey = (TertiaryTable ("Maximal","Implicit","Insertion")); + optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; optwrite = Impargs.make_maximal_implicit_args } @@ -849,7 +849,7 @@ let _ = declare_bool_option { optsync = true; optname = "coercion printing"; - optkey = (SecondaryTable ("Printing","Coercions")); + optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); optwrite = (fun b -> Constrextern.print_coercions := b) } @@ -857,14 +857,14 @@ let _ = declare_bool_option { optsync = true; optname = "printing of existential variable instances"; - optkey = (TertiaryTable ("Printing","Existential","Instances")); + optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Constrextern.print_evar_arguments); optwrite = (:=) Constrextern.print_evar_arguments } let _ = declare_bool_option { optsync = true; optname = "implicit arguments printing"; - optkey = (SecondaryTable ("Printing","Implicit")); + optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } @@ -872,7 +872,7 @@ let _ = declare_bool_option { optsync = true; optname = "implicit arguments defensive printing"; - optkey = (TertiaryTable ("Printing","Implicit","Defensive")); + optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } @@ -880,7 +880,7 @@ let _ = declare_bool_option { optsync = true; optname = "projection printing using dot notation"; - optkey = (SecondaryTable ("Printing","Projections")); + optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); optwrite = (fun b -> Constrextern.print_projections := b) } @@ -888,7 +888,7 @@ let _ = declare_bool_option { optsync = true; optname = "notations printing"; - optkey = (SecondaryTable ("Printing","Notations")); + optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } @@ -896,7 +896,7 @@ let _ = declare_bool_option { optsync = true; optname = "raw printing"; - optkey = (SecondaryTable ("Printing","All")); + optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } @@ -904,7 +904,7 @@ let _ = declare_bool_option { optsync = true; optname = "use of virtual machine inside the kernel"; - optkey = (SecondaryTable ("Virtual","Machine")); + optkey = ["Virtual";"Machine"]; optread = (fun () -> Vconv.use_vm ()); optwrite = (fun b -> Vconv.set_use_vm b) } @@ -912,7 +912,7 @@ let _ = declare_bool_option { optsync = true; optname = "use of boxed definitions"; - optkey = (SecondaryTable ("Boxed","Definitions")); + optkey = ["Boxed";"Definitions"]; optread = Flags.boxed_definitions; optwrite = (fun b -> Flags.set_boxed_definitions b) } @@ -920,60 +920,60 @@ let _ = declare_bool_option { optsync = true; optname = "use of boxed values"; - optkey = (SecondaryTable ("Boxed","Values")); + optkey = ["Boxed";"Values"]; optread = (fun _ -> not (Vm.transp_values ())); optwrite = (fun b -> Vm.set_transp_values (not b)) } let _ = declare_int_option - { optsync=false; - optkey=PrimaryTable("Undo"); - optname="the undo limit"; - optread=Pfedit.get_undo; - optwrite=Pfedit.set_undo } + { optsync = false; + optname = "the undo limit"; + optkey = ["Undo"]; + optread = Pfedit.get_undo; + optwrite = Pfedit.set_undo } let _ = declare_int_option - { optsync=false; - optkey=SecondaryTable("Hyps","Limit"); - optname="the hypotheses limit"; - optread=Flags.print_hyps_limit; - optwrite=Flags.set_print_hyps_limit } + { optsync = false; + optname = "the hypotheses limit"; + optkey = ["Hyps";"Limit"]; + optread = Flags.print_hyps_limit; + optwrite = Flags.set_print_hyps_limit } let _ = declare_int_option - { optsync=true; - optkey=SecondaryTable("Printing","Depth"); - optname="the printing depth"; - optread=Pp_control.get_depth_boxes; - optwrite=Pp_control.set_depth_boxes } + { optsync = true; + optname = "the printing depth"; + optkey = ["Printing";"Depth"]; + optread = Pp_control.get_depth_boxes; + optwrite = Pp_control.set_depth_boxes } let _ = declare_int_option - { optsync=true; - optkey=SecondaryTable("Printing","Width"); - optname="the printing width"; - optread=Pp_control.get_margin; - optwrite=Pp_control.set_margin } + { optsync = true; + optname = "the printing width"; + optkey = ["Printing";"Width"]; + optread = Pp_control.get_margin; + optwrite = Pp_control.set_margin } let _ = declare_bool_option - { optsync=true; - optkey=SecondaryTable("Printing","Universes"); - optname="printing of universes"; - optread=(fun () -> !Constrextern.print_universes); - optwrite=(fun b -> Constrextern.print_universes:=b) } + { optsync = true; + optname = "printing of universes"; + optkey = ["Printing";"Universes"]; + optread = (fun () -> !Constrextern.print_universes); + optwrite = (fun b -> Constrextern.print_universes:=b) } let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) let _ = declare_bool_option - { optsync=false; - optkey=SecondaryTable("Ltac","Debug"); - optname="Ltac debug"; - optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); - optwrite=vernac_debug } + { optsync = false; + optname = "Ltac debug"; + optkey = ["Ltac";"Debug"]; + optread = (fun () -> get_debug () <> Tactic_debug.DebugOff); + optwrite = vernac_debug } let vernac_set_opacity local str = let glob_ref r = diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 82a2a8449..63d93a767 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -42,7 +42,7 @@ let _ = declare_string_option { optsync = false; optname = "Whelp server"; - optkey = (SecondaryTable ("Whelp","Server")); + optkey = ["Whelp";"Server"]; optread = (fun () -> !whelp_server_name); optwrite = (fun s -> whelp_server_name := s) } @@ -50,7 +50,7 @@ let _ = declare_string_option { optsync = false; optname = "Whelp getter"; - optkey = (SecondaryTable ("Whelp","Getter")); + optkey = ["Whelp";"Getter"]; optread = (fun () -> !getter_server_name); optwrite = (fun s -> getter_server_name := s) } |