diff options
79 files changed, 280 insertions, 253 deletions
diff --git a/Makefile.common b/Makefile.common index 2367c14ea..f2148494f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -67,7 +67,7 @@ CONFIG:=\ LIBREP:=\ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.cmo \ - lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \ + lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/flags.cmo \ lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \ lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \ lib/predicate.cmo lib/rtree.cmo lib/heap.cmo lib/option.cmo @@ -348,7 +348,7 @@ MINICOQCMO:=$(CONFIG) $(LIBREP) $(KERNEL) \ GRAMMARNEEDEDCMO:=\ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.cmo \ - lib/dyn.cmo lib/options.cmo lib/hashcons.cmo lib/predicate.cmo \ + lib/dyn.cmo lib/flags.cmo lib/hashcons.cmo lib/predicate.cmo \ lib/rtree.cmo lib/option.cmo \ kernel/names.cmo kernel/univ.cmo \ kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \ diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml index 7cb4ad332..b2c94cd6f 100644 --- a/contrib/correctness/penv.ml +++ b/contrib/correctness/penv.ml @@ -233,7 +233,7 @@ let register id id' = try let (v,p) = Idmap.find id !edited in let _ = add_global id' v (Some p) in - Options.if_verbose + Flags.if_verbose msgnl (hov 0 (str"Program " ++ pr_id id' ++ spc () ++ str"is defined")); edited := Idmap.remove id !edited with Not_found -> () diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml index 23c1028a4..aaa304fe5 100644 --- a/contrib/correctness/pmisc.ml +++ b/contrib/correctness/pmisc.ml @@ -21,12 +21,12 @@ open Topconstr (* debug *) let deb_mess s = - if !Options.debug then begin + if !Flags.debug then begin msgnl s; pp_flush() end let deb_print f x = - if !Options.debug then begin + if !Flags.debug then begin msgnl (f x); pp_flush() end @@ -49,7 +49,7 @@ let reraise_with_loc loc f x = (* functions on names *) -let at = if !Options.v7 then "@" else "'at'" +let at = if !Flags.v7 then "@" else "'at'" let at_id id d = id_of_string ((string_of_id id) ^ at ^ d) diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index bb9a355c3..df1b67fd3 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -13,7 +13,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -open Options +open Flags open Util open Names open Nameops @@ -228,7 +228,7 @@ let mk_prog loc p pre post = loc = loc; info = () } -if !Options.v7 then +if !Flags.v7 then GEXTEND Gram (* Types ******************************************************************) diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index b99a3621d..76ba04c51 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -11,7 +11,7 @@ (* $Id$ *) open Pp -open Options +open Flags open Names open Libnames open Term diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 772a49742..abc7b1f04 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -305,7 +305,7 @@ let check_loaded_modfile mp = match base_mp mp with | _ -> () let info_file f = - Options.if_verbose message + Flags.if_verbose message ("The file "^f^" has been created by extraction.") diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 45976d6e5..a10241a7c 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -47,7 +47,7 @@ let observe_tac_stream s tac g = let observe_tac s tac g = observe_tac_stream (str s) tac g (* let tclTRYD tac = *) -(* if !Options.debug || do_observe () *) +(* if !Flags.debug || do_observe () *) (* then (fun g -> try (\* do_observe_tac "" *\)tac g with _ -> tclIDTAC g) *) (* else tac *) diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index 72f930b0a..160764799 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -384,7 +384,7 @@ let generate_functional_principle { const_entry_body = value; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() + const_entry_boxed = Flags.boxed_definitions() } in ignore( @@ -394,7 +394,7 @@ let generate_functional_principle Decl_kinds.IsDefinition (Decl_kinds.Scheme) ) ); - Options.if_verbose + Flags.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) name; names := name :: !names @@ -655,7 +655,7 @@ let build_scheme fas = (Declare.declare_constant princ_id (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); - Options.if_verbose + Flags.if_verbose (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id ) fas diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 3102f1b5d..612be05e3 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -354,14 +354,14 @@ let register_struct is_rec fixpoint_exprl = | [(fname,_,bl,ret_type,body),_] when not is_rec -> Command.declare_definition fname - (Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition) + (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition) bl None body (Some ret_type) (fun _ _ -> ()) | _ -> - Command.build_recursive fixpoint_exprl (Options.boxed_definitions()) + Command.build_recursive fixpoint_exprl (Flags.boxed_definitions()) let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index c2372d3ed..5ad4632e4 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -153,7 +153,7 @@ open Entries open Decl_kinds open Declare let definition_message id = - Options.if_verbose message ((string_of_id id) ^ " is defined") + Flags.if_verbose message ((string_of_id id) ^ " is defined") let save with_clean id const (locality,kind) hook = @@ -237,8 +237,8 @@ let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in - let old_rawprint = !Options.raw_print in - Options.raw_print := true; + let old_rawprint = !Flags.raw_print in + Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; Impargs.make_contextual_implicit_args false; @@ -247,14 +247,14 @@ let with_full_print f a = Impargs.make_implicit_args old_implicit_args; Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; - Options.raw_print := old_rawprint; + Flags.raw_print := old_rawprint; res with | e -> Impargs.make_implicit_args old_implicit_args; Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; - Options.raw_print := old_rawprint; + Flags.raw_print := old_rawprint; raise e diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml index cf6246704..44df08598 100644 --- a/contrib/funind/merge.ml +++ b/contrib/funind/merge.ml @@ -819,7 +819,7 @@ let rec merge_mutual_inductive_body let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *) - Options.with_option Options.raw_print (Constrextern.extern_rawtype Idset.empty) x + Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let params = prms2 @ prms1 in diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index af0a2addc..2f6f5914d 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -1181,8 +1181,8 @@ let do_build_inductive Array.map (List.map (fun (id,t) -> false,((dummy_loc,id), - Options.with_option - Options.raw_print + Flags.with_option + Flags.raw_print (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t) ) )) @@ -1218,7 +1218,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Options.silently (Command.build_mutual rel_inds)) true + with_full_print (Flags.silently (Command.build_mutual rel_inds)) true with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 30c96f939..a2da3b07d 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -783,7 +783,7 @@ let start_pcoq_mode debug = *) set_pcoq_hook pcoq_hook; start_pcoq_objects(); - Options.print_emacs := false; Pp.make_pp_nonemacs(); + Flags.print_emacs := false; Pp.make_pp_nonemacs(); end;; diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index a948dd4d6..26b6b3094 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -109,7 +109,7 @@ let (teq_id:identifier) = hyp_id 15 hyp_ids;; let (pmax_id:identifier) = hyp_id 16 hyp_ids;; let (hle_id:identifier) = hyp_id 17 hyp_ids;; -let message s = if Options.is_verbose () then msgnl(str s);; +let message s = if Flags.is_verbose () then msgnl(str s);; let def_of_const t = match (kind_of_term t) with @@ -948,7 +948,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_n (* (Array.make nb_goal ()) *) (* ; *) ref := Some lemma ; - Options.silently Vernacentries.interp (Vernacexpr.VernacAbort None); + Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None); build_proof ( fun gls -> let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in @@ -986,7 +986,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_n g); try by tclIDTAC; (* raises UserError _ if the proof is complete *) - if Options.is_verbose () then (pp (Printer.pr_open_subgoals())) + if Flags.is_verbose () then (pp (Printer.pr_open_subgoals())) with UserError _ -> defined () @@ -1306,7 +1306,7 @@ let (com_eqn : identifier -> ); (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) (* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) - Options.silently (fun () ->Command.save_named opacity) () ; + Flags.silently (fun () ->Command.save_named opacity) () ; (* Pp.msgnl (str "eqn finished"); *) );; @@ -1377,7 +1377,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; - if Options.is_verbose () + if Flags.is_verbose () then msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ h 1 (Ppconstr.pr_id equation_id ++ diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 97dd2f143..84568588c 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -12,7 +12,7 @@ open Pp open Util -open Options +open Flags open Term open Names open Libnames diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index a3d95ab62..d1b4b50eb 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -14,7 +14,7 @@ open Util open Subtac_utils let trace s = - if !Options.debug then (msgnl s; msgerr s) + if !Flags.debug then (msgnl s; msgerr s) else () let succfix (depth, fixrels) = diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 7fd08c7b0..c2691c781 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -17,7 +17,7 @@ (* $Id$ *) -open Options +open Flags open Util open Names open Nameops diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 4617ca977..4f5e302c2 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -76,7 +76,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook = let _ = Typeops.infer_type env c in Command.start_proof id kind c hook -let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () +let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () let start_proof_and_print env isevars idopt k t hook = start_proof_com env isevars idopt k t hook; @@ -85,7 +85,7 @@ let start_proof_and_print env isevars idopt k t hook = let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) let assumption_message id = - Options.if_verbose message ((string_of_id id) ^ " is assumed") + Flags.if_verbose message ((string_of_id id) ^ " is assumed") let declare_assumption env isevars idl is_coe k bl c nl = if not (Pfedit.refining ()) then diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 49eab5d29..a9a30c57a 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -349,7 +349,7 @@ let build_mutrec lnameargsardef boxed = ([],env,[],[]) lnameargsardef in let arityl = List.rev arityl in let notations = - List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) + List.fold_right (fun (_,ntnopt) l -> Option.List.cons ntnopt l) lnameargsardef [] in let recdef = diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 5e7f025be..e3cf7a57a 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -43,7 +43,7 @@ type program_info = { } let assumption_message id = - Options.if_verbose message ((string_of_id id) ^ " is assumed") + Flags.if_verbose message ((string_of_id id) ^ " is assumed") let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ()) @@ -248,11 +248,11 @@ type progress = let obligations_message rem = if rem > 0 then if rem = 1 then - Options.if_verbose msgnl (int rem ++ str " obligation remaining") + Flags.if_verbose msgnl (int rem ++ str " obligation remaining") else - Options.if_verbose msgnl (int rem ++ str " obligations remaining") + Flags.if_verbose msgnl (int rem ++ str " obligations remaining") else - Options.if_verbose msgnl (str "No more obligations remaining") + Flags.if_verbose msgnl (str "No more obligations remaining") let update_obls prg obls rem = let prg' = { prg with prg_obligations = (obls, rem) } in @@ -390,21 +390,21 @@ and try_solve_obligations n tac = try ignore (solve_obligations n tac) with NoObligations _ -> () and auto_solve_obligations n : progress = - Options.if_verbose msgnl (str "Solving obligations automatically..."); + Flags.if_verbose msgnl (str "Solving obligations automatically..."); try solve_obligations n !default_tactic with NoObligations _ -> Dependent let add_definition n b t obls = - Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); + Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); let prg = init_prog_info n b t [] (Array.make 0 0) obls in let obls,_ = prg.prg_obligations in if Array.length obls = 0 then ( - Options.if_verbose ppnl (str "."); + Flags.if_verbose ppnl (str "."); let cst = declare_definition prg in from_prg := ProgMap.remove prg.prg_name !from_prg; Defined cst) else ( let len = Array.length obls in - let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in + let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in from_prg := ProgMap.add n prg !from_prg; auto_solve_obligations (Some n)) diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 44638f496..d5df9adc9 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -113,20 +113,20 @@ let debug_on = true let debug n s = if debug_on then - if !Options.debug && n >= debug_level then + if !Flags.debug && n >= debug_level then msgnl s else () else () let debug_msg n s = if debug_on then - if !Options.debug && n >= debug_level then s + if !Flags.debug && n >= debug_level then s else mt () else mt () let trace s = if debug_on then - if !Options.debug && debug_level > 0 then msgnl s + if !Flags.debug && debug_level > 0 then msgnl s else () else () @@ -353,7 +353,7 @@ let recursive_message v = spc () ++ str "are recursively defined") let print_message m = - Options.if_verbose ppnl m + Flags.if_verbose ppnl m (* Solve an obligation using tactics, return the corresponding proof term *) let solve_by_tac evi t = diff --git a/dev/top_printers.ml b/dev/top_printers.ml index cd0fa0c0d..27577c79c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -48,7 +48,7 @@ let ppqualid qid = pp(pr_qualid qid) (* term printers *) let ppconstr x = pp (Termops.print_constr x) -let ppconstrdb x = pp(Options.with_option Constrextern.rawdebug Termops.print_constr x) +let ppconstrdb x = pp(Flags.with_option Constrextern.rawdebug Termops.print_constr x) let ppterm = ppconstr let ppsconstr x = ppconstr (Declarations.force x) let ppconstr_univ x = Constrextern.with_universes ppconstr x diff --git a/ide/coq.ml b/ide/coq.ml index 50536491c..128717acf 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -43,7 +43,7 @@ let init () = Problem: should not hide "xx is assumed" messages *) (**) - Options.make_silent true; + Flags.make_silent true; (**) Coqtop.init_ide () @@ -156,11 +156,11 @@ let interp verbosely s = | VernacExtend("Extraction", _) | VernacExtend("ExtractionLibrary",_) | VernacExtend("RecursiveExtractionLibrary",_) - -> Options.make_silent (not verbosely) + -> Flags.make_silent (not verbosely) | _ -> () end; Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); - Options.make_silent true; + Flags.make_silent true; prerr_endline ("...Done with interp of : "^s); last diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 0c2e3905d..b79e4b936 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -25,7 +25,7 @@ let set_location = ref (function s -> failwith "not ready") let pulse = ref (function () -> failwith "not ready") -let debug = Options.debug +let debug = Flags.debug let prerr_endline s = if !debug then (prerr_endline s;flush stderr) @@ -35,7 +35,7 @@ let prerr_string s = let lib_ide_file f = let coqlib = System.getenv_else "COQLIB" - (if Coq_config.local || !Options.boot then Coq_config.coqtop + (if Coq_config.local || !Flags.boot then Coq_config.coqtop else Coq_config.coqlib) in Filename.concat (Filename.concat coqlib "ide") f diff --git a/ide/preferences.ml b/ide/preferences.ml index fdfd7720d..d03afa3a9 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -127,7 +127,7 @@ let (current:pref ref) = modifiers_valid = [`SHIFT; `CONTROL; `MOD1]; - cmd_browse = Options.browser_cmd_fmt; + cmd_browse = Flags.browser_cmd_fmt; cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD ", "" diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml index 14ec6d8cc..37f2e9a4a 100644 --- a/ide/utils/config_file.ml +++ b/ide/utils/config_file.ml @@ -552,7 +552,7 @@ class filename_cp = string_cp (* ******************************************************************************** *) -(******************** Backward compatibility with module Options ****************** *) +(******************** Backward compatibility with module Flags.****************** *) (* ******************************************************************************** *) type 'a option_class = 'a wrappers diff --git a/ide/utils/uoptions.ml b/ide/utils/uoptions.ml index 416f57696..aa3b42cd0 100644 --- a/ide/utils/uoptions.ml +++ b/ide/utils/uoptions.ml @@ -24,7 +24,7 @@ (** Simple options: This will enable very simple configuration, by a mouse-based configurator. - Options will be defined by a special function, which will also check + Flags.will be defined by a special function, which will also check if a value has been provided by the user in its .gwmlrc file. The .gwmlrc will be created by a dedicated tool, which could be used to generate both .gwmlrc and .efunsrc files. @@ -151,7 +151,7 @@ let opfile.file_rc) with Not_found -> default_value | e -> - Printf.printf "Options.define_option, for option %s: " + Printf.printf "Flags.define_option, for option %s: " (match option_name with [] -> "???" | name :: _ -> name); @@ -344,7 +344,7 @@ let value_to_string v = StringValue s -> s | IntValue i -> string_of_int i | FloatValue f -> string_of_float f - | _ -> failwith "Options: not a string option" + | _ -> failwith "Flags. not a string option" ;; let string_to_value s = StringValue s;; @@ -353,7 +353,7 @@ let value_to_int v = match v with StringValue s -> int_of_string s | IntValue i -> i - | _ -> failwith "Options: not an int option" + | _ -> failwith "Flags. not an int option" ;; let int_to_value i = IntValue i;; @@ -375,7 +375,7 @@ let value_to_bool v = StringValue s -> bool_of_string s | IntValue v when v = 0 -> false | IntValue v when v = 1 -> true - | _ -> failwith "Options: not a bool option" + | _ -> failwith "Flags. not a bool option" ;; let bool_to_value i = StringValue (string_of_bool i);; @@ -383,7 +383,7 @@ let value_to_float v = match v with StringValue s -> float_of_string s | FloatValue f -> f - | _ -> failwith "Options: not a float option" + | _ -> failwith "Flags. not a float option" ;; let float_to_value i = FloatValue i;; @@ -392,7 +392,7 @@ let value_to_string2 v = match v with List [s1; s2] | SmallList [s1;s2] -> value_to_string s1, value_to_string s2 - | _ -> failwith "Options: not a string2 option" + | _ -> failwith "Flags. not a string2 option" ;; let string2_to_value (s1, s2) = SmallList [StringValue s1; StringValue s2];; @@ -401,10 +401,10 @@ let value_to_list v2c v = match v with List l | SmallList l -> List.rev (List.rev_map v2c l) | StringValue s -> failwith (Printf.sprintf - "Options: not a list option (StringValue [%s])" s) - | FloatValue _ -> failwith "Options: not a list option (FloatValue)" - | IntValue _ -> failwith "Options: not a list option (IntValue)" - | Module _ -> failwith "Options: not a list option (Module)" + "Flags. not a list option (StringValue [%s])" s) + | FloatValue _ -> failwith "Flags. not a list option (FloatValue)" + | IntValue _ -> failwith "Flags. not a list option (IntValue)" + | Module _ -> failwith "Flags. not a list option (Module)" ;; let list_to_value c2v l = @@ -458,7 +458,7 @@ let from_value cl = cl.from_value;; let value_to_sum l v = match v with StringValue s -> List.assoc s l - | _ -> failwith "Options: not a sum option" + | _ -> failwith "Flags. not a sum option" ;; let sum_to_value l v = StringValue (List.assq v l);; @@ -659,8 +659,8 @@ let value_to_tuple2 (c1, c2) v = | List l | SmallList l -> Printf.printf "list of %d" (List.length l); print_newline (); - failwith "Options: not a tuple2 list option" - | _ -> failwith "Options: not a tuple2 option" + failwith "Flags. not a tuple2 list option" + | _ -> failwith "Flags. not a tuple2 option" ;; let tuple2_option p = @@ -675,7 +675,7 @@ let value_to_tuple3 (c1, c2, c3) v = List [v1; v2; v3] -> from_value c1 v1, from_value c2 v2, from_value c3 v3 | SmallList [v1; v2; v3] -> from_value c1 v1, from_value c2 v2, from_value c3 v3 - | _ -> failwith "Options: not a tuple3 option" + | _ -> failwith "Flags. not a tuple3 option" ;; let tuple3_option p = @@ -691,7 +691,7 @@ let value_to_tuple4 (c1, c2, c3, c4) v = (from_value c1 v1, from_value c2 v2, from_value c3 v3, from_value c4 v4) | SmallList [v1; v2; v3; v4] -> (from_value c1 v1, from_value c2 v2, from_value c3 v3, from_value c4 v4) - | _ -> failwith "Options: not a tuple4 option" + | _ -> failwith "Flags. not a tuple4 option" ;; let tuple4_option p = diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ec74c91b2..1117d2507 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -67,12 +67,12 @@ let print_projections = ref false let print_meta_as_hole = ref false -let with_arguments f = Options.with_option print_arguments f -let with_implicits f = Options.with_option print_implicits f -let with_coercions f = Options.with_option print_coercions f -let with_universes f = Options.with_option print_universes f -let without_symbols f = Options.with_option print_no_symbol f -let with_meta_as_hole f = Options.with_option print_meta_as_hole f +let with_arguments f = Flags.with_option print_arguments f +let with_implicits f = Flags.with_option print_implicits f +let with_coercions f = Flags.with_option print_coercions f +let with_universes f = Flags.with_option print_universes f +let without_symbols f = Flags.with_option print_no_symbol f +let with_meta_as_hole f = Flags.with_option print_meta_as_hole f (**********************************************************************) (* Various externalisation functions *) @@ -409,7 +409,7 @@ let match_aconstr_cases_pattern c (metas_scl,pat) = (* Better to use extern_rawconstr composed with injection/retraction ?? *) let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try - if !Options.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print or !print_no_symbol then raise No_match; let (na,sc,p) = uninterp_prim_token_cases_pattern pat in match availability_of_prim_token sc scopes with | None -> raise No_match @@ -418,7 +418,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na with No_match -> try - if !Options.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print or !print_no_symbol then raise No_match; extern_symbol_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> @@ -451,7 +451,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes' = option_cons scopt scopes in + let scopes' = Option.List.cons scopt scopes in let l = List.map (fun (c,(scopt,scl)) -> extern_cases_pattern_in_scope (scopt,scl@scopes') vars c) @@ -476,7 +476,7 @@ let occur_name na aty = | Anonymous -> false let is_projection nargs = function - | Some r when not !Options.raw_print & !print_projections -> + | Some r when not !Flags.raw_print & !print_projections -> (try let n = Recordops.find_projection_nparams r + 1 in if n <= nargs then Some n else None @@ -496,7 +496,7 @@ let explicitize loc inctx impl (cf,f) args = | a::args, imp::impl when is_status_implicit imp -> let tail = exprec (q+1) (args,impl) in let visible = - !Options.raw_print or + !Flags.raw_print or (!print_implicits & !print_implicits_explicit_args) or (!print_implicits_defensive & is_significant_implicit a impl tail & @@ -535,7 +535,7 @@ let extern_app loc inctx impl (cf,f) args = extern_global loc impl f else if - ((!Options.raw_print or + ((!Flags.raw_print or (!print_implicits & not !print_implicits_explicit_args)) & List.exists is_status_implicit impl) then @@ -554,7 +554,7 @@ let rec extern_args extern scopes env args subscopes = let rec remove_coercions inctx = function | RApp (loc,RRef (_,r),args) as c - when not (!Options.raw_print or !print_coercions) + when not (!Flags.raw_print or !print_coercions) -> let nargs = List.length args in (try match Classops.hide_coercion r with @@ -638,11 +638,11 @@ let extern_rawsort = function let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try - if !Options.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print or !print_no_symbol then raise No_match; extern_optimal_prim_token scopes r r' with No_match -> try - if !Options.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print or !print_no_symbol then raise No_match; extern_symbol scopes vars r' (uninterp_notations r') with No_match -> match r' with | RRef (loc,ref) -> @@ -772,7 +772,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes) and factorize_prod scopes vars aty c = try - if !Options.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print or !print_no_symbol then raise No_match; ([],extern_symbol scopes vars c (uninterp_notations c)) with No_match -> match c with | RProd (loc,(Name id as na),ty,c) @@ -784,7 +784,7 @@ and factorize_prod scopes vars aty c = and factorize_lambda inctx scopes vars aty c = try - if !Options.raw_print or !print_no_symbol then raise No_match; + if !Flags.raw_print or !print_no_symbol then raise No_match; ([],extern_symbol scopes vars c (uninterp_notations c)) with No_match -> match c with | RLambda (loc,na,ty,c) @@ -845,7 +845,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | None -> raise No_match (* Uninterpretation is allowed in current context *) | Some (scopt,key) -> - let scopes' = option_cons scopt scopes in + let scopes' = Option.List.cons scopt scopes in let l = List.map (fun (c,(scopt,scl)) -> extern (* assuming no overloading: *) true diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6fc7a7d31..a41825346 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -10,7 +10,7 @@ open Pp open Util -open Options +open Flags open Names open Nameops open Libnames @@ -221,7 +221,7 @@ let contract_pat_notation ntn l = (**********************************************************************) (* Remembering the parsing scope of variables in notations *) -let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes +let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes let set_var_scope loc id (_,scopt,scopes) varscopes = let idscopes = List.assoc id varscopes in diff --git a/interp/notation.ml b/interp/notation.ml index d5de23bc5..b04f3be03 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -73,7 +73,7 @@ let init_scope_map () = let declare_scope scope = try let _ = Gmap.find scope !scope_map in () with Not_found -> -(* Options.if_verbose message ("Creating scope "^scope);*) +(* Flags.if_verbose message ("Creating scope "^scope);*) scope_map := Gmap.add scope empty_scope !scope_map let find_scope scope = @@ -142,16 +142,16 @@ let delimiters_map = ref Gmap.empty let declare_delimiters scope key = let sc = find_scope scope in - if sc.delimiters <> None && Options.is_verbose () then begin + if sc.delimiters <> None && Flags.is_verbose () then begin let old = Option.get sc.delimiters in - Options.if_verbose + Flags.if_verbose warning ("Overwritting previous delimiting key "^old^" in scope "^scope) end; let sc = { sc with delimiters = Some key } in scope_map := Gmap.add scope sc !scope_map; if Gmap.mem key !delimiters_map then begin let oldsc = Gmap.find key !delimiters_map in - Options.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc) + Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc) end; delimiters_map := Gmap.add key scope !delimiters_map @@ -300,7 +300,7 @@ let declare_notation_interpretation ntn scopt pat df = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in if Gmap.mem ntn sc.notations then - Options.if_warn msg_warning (str ("Notation "^ntn^" was already used"^ + Flags.if_warn msg_warning (str ("Notation "^ntn^" was already used"^ (if scopt = None then "" else " in scope "^scope))); let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in scope_map := Gmap.add scope sc !scope_map; @@ -637,7 +637,7 @@ let error_notation_not_reference loc ntn = let interp_notation_as_global_reference loc test ntn = let ntns = browse_notation true ntn !scope_map in let refs = List.map (global_reference_of_notation test) ntns in - match filter_some refs with + match Option.List.flatten refs with | [_,_,ref] -> ref | [] -> error_notation_not_reference loc ntn | refs -> diff --git a/interp/reserve.ml b/interp/reserve.ml index 131ce2970..02e15f069 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -85,7 +85,7 @@ let rec unloc = function let anonymize_if_reserved na t = match na with | Name id as na -> (try - if not !Options.raw_print & unloc t = find_reserved_type id + if not !Flags.raw_print & unloc t = find_reserved_type id then RHole (dummy_loc,Evd.BinderType na) else t with Not_found -> t) diff --git a/lib/options.ml b/lib/flags.ml index 589069567..12b2ed037 100644 --- a/lib/options.ml +++ b/lib/flags.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: options.ml 10106 2007-08-30 16:56:10Z herbelin $ *) open Util @@ -100,13 +100,13 @@ let dump_it () = let _ = at_exit dump_it -(* Options for the virtual machine *) +(* Flags.for the virtual machine *) let boxed_definitions = ref true let set_boxed_definitions b = boxed_definitions := b let boxed_definitions _ = !boxed_definitions -(* Options for external tools *) +(* Flags.for external tools *) let browser_cmd_fmt = try diff --git a/lib/options.mli b/lib/flags.mli index 73962735d..248b59b0d 100644 --- a/lib/options.mli +++ b/lib/flags.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: options.mli 9679 2007-02-24 15:22:07Z herbelin $ i*) (* Global options of the system. *) diff --git a/lib/option.ml b/lib/option.ml index 0ed36b002..436358b55 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -32,6 +32,14 @@ let get = function (** [make x] returns [Some x]. *) let make x = Some x +(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *) +let init b x = + if b then + Some x + else + None + + (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) let flatten = function | Some (Some y) -> Some y @@ -120,3 +128,22 @@ let lift2 f x y = match x,y with | Some z, Some w -> Some (f z w) | _,_ -> None + + + +(** {6 Operations with Lists} *) + +module List = + struct + (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *) + let cons x l = + match x with + | Some y -> y::l + | _ -> l + + (** [List.flatten l] is the list of all the [y]s such that [l] contains + [Some y] (in the same order). *) + let rec flatten = function + | x::l -> cons x (flatten l) + | [] -> [] +end diff --git a/lib/option.mli b/lib/option.mli index f98c45ee7..8e768d8af 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -28,6 +28,9 @@ val get : 'a option -> 'a (** [make x] returns [Some x]. *) val make : 'a -> 'a option +(** [init b x] returns [Some x] if [b] is [true] and [None] otherwise. *) +val init : bool -> 'a -> 'a option + (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) val flatten : 'a option option -> 'a option @@ -64,7 +67,7 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b -(** {6 More Specific operations} ***) +(** {6 More Specific Operations} ***) (** [default f x a] is [f y] if [x] is [Some y] and [a] otherwise. *) val default : ('a -> 'b) -> 'a option -> 'b -> 'b @@ -83,3 +86,15 @@ val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option (** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals [Some w]. It is [None] otherwise. *) val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option + + +(** {6 Operations with Lists} *) + +module List : sig + (** [List.cons x l] equals [y::l] if [x] is [Some y] and [l] otherwise. *) + val cons : 'a option -> 'a list -> 'a list + + (** [List.flatten l] is the list of all the [y]s such that [l] contains + [Some y] (in the same order). *) + val flatten : 'a option list -> 'a list +end diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 415a3002a..067c52700 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -11,10 +11,10 @@ open Pp_control (* This should not be used outside of this file. Use - Options.print_emacs instead. This one is updated when reading + Flags.print_emacs instead. This one is updated when reading command line options. This was the only way to make [Pp] depend on - an option without creating a circularity: [Options] -> [Util] -> - [Pp] -> [Options] *) + an option without creating a circularity: [Flags. -> [Util] -> + [Pp] -> [Flags. *) let print_emacs = ref false let make_pp_emacs() = print_emacs:=true let make_pp_nonemacs() = print_emacs:=false diff --git a/lib/util.ml b/lib/util.ml index b61cd88ff..99a203d52 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -788,19 +788,11 @@ let interval n m = in interval_n ([],m) -let option_cons a l = match a with - | Some x -> x::l - | None -> l - let option_compare f a b = match (a,b) with | None, None -> true | Some a', Some b' -> f a' b' | _ -> failwith "option_compare" -let rec filter_some = function - | [] -> [] - | None::l -> filter_some l - | Some a::l -> a :: filter_some l let map_succeed f = let rec map_f = function diff --git a/lib/util.mli b/lib/util.mli index 71262bb4c..331363f0a 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -223,9 +223,7 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list val interval : int -> int -> int list -val option_cons : 'a option -> 'a list -> 'a list val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool -val filter_some : 'a option list -> 'a list (* In [map_succeed f l] an element [a] is removed if [f a] raises *) (* [Failure _] otherwise behaves as [List.map f l] *) diff --git a/library/declare.ml b/library/declare.ml index 65d08dd81..da2c1b778 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -47,7 +47,7 @@ let xml_declare_variable = ref (fun (sp:object_name) -> ()) let xml_declare_constant = ref (fun (sp:bool * constant)-> ()) let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ()) -let if_xml f x = if !Options.xml_export then f x else () +let if_xml f x = if !Flags.xml_export then f x else () let set_xml_declare_variable f = xml_declare_variable := if_xml f let set_xml_declare_constant f = xml_declare_constant := if_xml f @@ -196,7 +196,7 @@ let (in_constant, out_constant) = export_function = export_constant } let hcons_constant_declaration = function - | DefinitionEntry ce when !Options.hash_cons_proofs -> + | DefinitionEntry ce when !Flags.hash_cons_proofs -> let (hcons1_constr,_) = hcons_constr (hcons_names()) in DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; diff --git a/library/goptions.ml b/library/goptions.ml index 4be15569e..b614ed34a 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -208,7 +208,7 @@ module MakeRefTable = functor (A : RefConvertArg) -> MakeTable (RefConvert(A)) (****************************************************************************) -(* 2- Options *) +(* 2- Flags. *) type 'a option_sig = { optsync : bool; diff --git a/library/lib.ml b/library/lib.ml index 50bef5a5d..8fff32e1a 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -503,7 +503,7 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; - if !Options.xml_export then !xml_open_section id; + if !Flags.xml_export then !xml_open_section id; add_section () @@ -536,7 +536,7 @@ let close_section id = let full_olddir = fst !path_prefix in pop_path_prefix (); add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening))); - if !Options.xml_export then !xml_close_section id; + if !Flags.xml_export then !xml_close_section id; let newdecls = List.map discharge_item secdecls in Summary.section_unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; diff --git a/library/library.ml b/library/library.ml index ced150f7b..e53c0cd1a 100644 --- a/library/library.ml +++ b/library/library.ml @@ -86,7 +86,7 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> Nameops.default_root_prefix then - Options.if_warn msg_warning + Flags.if_warn msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); @@ -386,7 +386,7 @@ let try_locate_qualified_library (loc,qid) = (* Internalise libraries *) let lighten_library m = - if !Options.dont_load_proofs then lighten_library m else m + if !Flags.dont_load_proofs then lighten_library m else m let mk_library md f digest = { library_name = md.md_name; @@ -449,7 +449,7 @@ let rec_intern_by_filename_only id f = (* We check no other file containing same library is loaded *) try let m' = find_library m.library_name in - Options.if_verbose warning + Flags.if_verbose warning ((string_of_dirpath m.library_name)^" is already loaded from file "^ m'.library_filename); m.library_name, [] @@ -536,7 +536,7 @@ let require_library qidl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); - if !Options.xml_export then List.iter !xml_require modrefl; + if !Flags.xml_export then List.iter !xml_require modrefl; add_frozen_state () let require_library_from_file idopt file export = @@ -549,7 +549,7 @@ let require_library_from_file idopt file export = end else add_anonymous_leaf (in_require (needed,[modref],export)); - if !Options.xml_export then !xml_require modref; + if !Flags.xml_export then !xml_require modref; add_frozen_state () (* the function called by Vernacentries.vernac_import *) diff --git a/library/nametab.ml b/library/nametab.ml index 395b2159f..9aab07cac 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -107,7 +107,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Options.if_verbose + Flags.if_verbose warning ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"); current @@ -147,7 +147,7 @@ let rec push_exactly uname o level (current,dirmap) = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - Options.if_verbose + Flags.if_verbose warning ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!"); current diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml index 8b8761cb1..c62c81377 100644 --- a/parsing/g_natsyntax.ml +++ b/parsing/g_natsyntax.ml @@ -33,7 +33,7 @@ open Names let nat_of_int dloc n = if is_pos_or_zero n then begin if less_than (of_string "5000") n then - Options.if_warn msg_warning + Flags.if_warn msg_warning (strbrk "Stack overflow or segmentation fault happens when " ++ strbrk "working with large numbers in nat (observed threshold " ++ strbrk "may vary from 5000 to 70000 depending on your system " ++ diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a7a78f770..729693aa7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -105,7 +105,7 @@ END let test_plurial_form = function | [(_,([_],_))] -> - Options.if_verbose warning + Flags.if_verbose warning "Keywords Variables/Hypotheses/Parameters expect more than one assumption" | _ -> () @@ -143,7 +143,7 @@ GEXTEND Gram | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (recs,false) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (recs,Options.boxed_definitions()) + VernacFixpoint (recs,Flags.boxed_definitions()) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> VernacCoFixpoint (corecs,false) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l @@ -175,11 +175,11 @@ GEXTEND Gram ; def_token: [ [ "Definition" -> - no_hook, (Global, Options.boxed_definitions(), Definition) + no_hook, (Global, Flags.boxed_definitions(), Definition) | IDENT "Let" -> - no_hook, (Local, Options.boxed_definitions(), Definition) + no_hook, (Local, Flags.boxed_definitions(), Definition) | IDENT "Example" -> - no_hook, (Global, Options.boxed_definitions(), Example) + no_hook, (Global, Flags.boxed_definitions(), Example) | IDENT "SubClass" -> Class.add_subclass_hook, (Global, false, SubClass) | IDENT "Local"; IDENT "SubClass" -> Class.add_subclass_hook, (Local, false, SubClass) ] ] diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index cfa62fa5a..a711bb85a 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -374,10 +374,10 @@ let null_comment s = let comment_stop ep = let current_s = Buffer.contents current in - if !Options.xml_export && Buffer.length current > 0 && + if !Flags.xml_export && Buffer.length current > 0 && (!between_com || not(null_comment current_s)) then !xml_output_comment current_s; - (if Options.do_translate() && Buffer.length current > 0 && + (if Flags.do_translate() && Buffer.length current > 0 && (!between_com || not(null_comment current_s)) then let bp = match !comment_begin with Some bp -> bp @@ -412,7 +412,7 @@ let rec comment bp = parser bp2 | [< '')' >] -> push_string "*)"; | [< s >] -> real_push_char '*'; comment bp s >] -> () | [< ''"'; s >] -> - if Options.do_translate() then (push_string"\"";comm_string bp2 s) + if Flags.do_translate() then (push_string"\"";comm_string bp2 s) else ignore (string bp2 0 s); comment bp s | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment @@ -485,7 +485,7 @@ let rec next_token = parser bp (("METAIDENT", get_buff len), (bp,ep)) | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep -> comment_stop bp; - if Options.do_translate() & t=("",".") then between_com := true; + if Flags.do_translate() & t=("",".") then between_com := true; (t, (bp,ep)) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ep -> diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 07055869a..d2380dad6 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -162,7 +162,7 @@ let camlp4_verbosity silent f x = let grammar_extend te pos rls = camlp4_state := ByGrammar (Gramobj.weaken_entry te,pos,rls) :: !camlp4_state; - camlp4_verbosity (Options.is_verbose ()) (G.extend te pos) rls + camlp4_verbosity (Flags.is_verbose ()) (G.extend te pos) rls (* n is the number of extended entries (not the number of Grammar commands!) to remove. *) diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 8e542ce14..858c6685f 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -96,13 +96,13 @@ let pr_delimiters key strm = strm ++ str ("%"^key) let pr_located pr (loc,x) = - if Options.do_translate() && loc<>dummy_loc then + if Flags.do_translate() && loc<>dummy_loc then let (b,e) = unloc loc in comment b ++ pr x ++ comment e else pr x let pr_com_at n = - if Options.do_translate() && n <> 0 then comment n + if Flags.do_translate() && n <> 0 then comment n else mt() let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index bbb481f3e..1161c3b61 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -570,7 +570,7 @@ let rec pr_vernac = function let pr_onerec = function | (id,(n,ro),bl,type_,def),ntn -> let (bl',def,type_) = - if Options.do_translate() then extract_def_binders def type_ + if Flags.do_translate() then extract_def_binders def type_ else ([],def,type_) in let bl = bl @ bl' in let ids = List.flatten (List.map name_of_binder bl) in @@ -607,7 +607,7 @@ let rec pr_vernac = function | VernacCoFixpoint (corecs,b) -> let pr_onecorec ((id,bl,c,def),ntn) = let (bl',def,c) = - if Options.do_translate() then extract_def_binders def c + if Flags.do_translate() then extract_def_binders def c else ([],def,c) in let bl = bl @ bl' in pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ @@ -753,7 +753,7 @@ let rec pr_vernac = function (Global.env()) body in hov 1 - (((*if !Options.p1 then + (((*if !Flags.p1 then (if rc then str "Recursive " else mt()) ++ str "Tactic Definition " else*) (* Rec by default *) str "Ltac ") ++ diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index a3a0c2f15..9beba9347 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -352,7 +352,7 @@ let gallina_print_inductive sp = let (mib,mip) = Global.lookup_inductive (sp,0) in let mipv = mib.mind_packets in let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in - (if mib.mind_record & not !Options.raw_print then + (if mib.mind_record & not !Flags.raw_print then pr_record (List.hd names) else pr_mutual_inductive mib.mind_finite names) ++ fnl () ++ diff --git a/parsing/printer.ml b/parsing/printer.ml index 52e5cb836..ac2155098 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -30,7 +30,7 @@ open Ppconstr open Constrextern let emacs_str s alts = - match !Options.print_emacs, !Options.print_emacs_safechar with + match !Flags.print_emacs, !Flags.print_emacs_safechar with | true, true -> alts | true , false -> s | false,_ -> "" @@ -227,7 +227,7 @@ let pr_context_limit n env = in (sign_env ++ db_env) -let pr_context_of env = match Options.print_hyps_limit () with +let pr_context_of env = match Flags.print_hyps_limit () with | None -> hv 0 (pr_context_unlimited env) | Some n -> hv 0 (pr_context_limit n env) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 9a628b3fd..5b0c2eb36 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -10,7 +10,7 @@ open Util open Pp -open Options +open Flags open Names open Libnames open Nametab diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f3468bcbf..729bd84f1 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -262,7 +262,7 @@ module Default = struct (* a little more effort to get products is needed *) try decompose_prod_n nabs t with _ -> - if !Options.debug then + if !Flags.debug then msg_warning (str "decompose_prod_n failed"); raise (Invalid_argument "Coercion.inh_conv_coerces_to") in diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 9dfe393be..2cfa7076a 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -108,7 +108,7 @@ module PrintingCasesLet = module PrintingIf = Goptions.MakeRefTable(PrintingCasesIf) module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet) -(* Options for printing or not wildcard and synthetisable types *) +(* Flags.for printing or not wildcard and synthetisable types *) open Goptions @@ -299,7 +299,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let synth_type = synthetize_type () in let tomatch = detype c in let alias, aliastyp, pred= - if (not !Options.raw_print) & synth_type & computable & Array.length bl<>0 + if (not !Flags.raw_print) & synth_type & computable & Array.length bl<>0 then Anonymous, None, None else @@ -319,7 +319,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = let eqnl = detype_eqns constructs consnargsl bl in let tag = try - if !Options.raw_print then + if !Flags.raw_print then RegularStyle else if PrintingLet.active (indsp,consnargsl) then LetStyle @@ -471,7 +471,7 @@ and share_names isgoal n l avoid env c t = and detype_eqns isgoal avoid env ci computable constructs consnargsl bl = try - if !Options.raw_print or not (reverse_matching ()) then raise Exit; + if !Flags.raw_print or not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous isgoal (avoid,env) ci bl in List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c)) mat diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 84f35241a..b894a9aae 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -157,7 +157,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = (match dest_recarg ra with | Mrec j when is_rec -> (depPvect.(j),rest) | Imbr _ -> - Options.if_verbose warning "Ignoring recursive call"; + Flags.if_verbose warning "Ignoring recursive call"; (None,rest) | _ -> (None, rest)) in diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index d64e84fea..63dfbb2d9 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -234,7 +234,7 @@ let rec pat_of_raw metas vars = function | RHole _ -> PMeta None | RCast (_,c,_) -> - Options.if_verbose + Flags.if_verbose Pp.warning "Cast not taken into account in constr pattern"; pat_of_raw metas vars c | RIf (_,c,(_,None),b1,b2) -> diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index c4c9894cb..60664f199 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -755,11 +755,11 @@ let rec substlin env name n ol c = (n2,ol2,mkCast (c1',k,c2'))) | Fix _ -> - (Options.if_verbose + (Flags.if_verbose warning "do not consider occurrences inside fixpoints"; (n,ol,c)) | CoFix _ -> - (Options.if_verbose + (Flags.if_verbose warning "do not consider occurrences inside cofixpoints"; (n,ol,c)) | (Rel _|Meta _|Var _|Sort _ diff --git a/proofs/logic.ml b/proofs/logic.ml index 4c6e5bacf..136f61343 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -59,7 +59,7 @@ let rec catchable_exception = function (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) let check = ref false -let with_check = Options.with_option check +let with_check = Flags.with_option check (************************************************************************) (************************************************************************) diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index 5d35298e8..aeeb2e134 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -134,7 +134,7 @@ let all_subdirs dir = (* usage *) let usage () = prerr_endline "Usage: coqmktop <options> <ocaml options> files -Options are: +Flags.are: -srcdir dir Specify where the Coq source files are -o exec-file Specify the name of the resulting toplevel -opt Compile in native code diff --git a/tactics/auto.ml b/tactics/auto.ml index 8bce850db..480ca9560 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -230,7 +230,7 @@ let make_resolves env sigma eap c = let ents = map_succeed (fun f -> f (c,cty)) - [make_exact_entry; make_apply_entry env sigma (eap,Options.is_verbose())] + [make_exact_entry; make_apply_entry env sigma (eap,Flags.is_verbose())] in if ents = [] then errorlabstrm "Hint" diff --git a/tactics/leminv.ml b/tactics/leminv.ml index f34c9e38d..b43466e31 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -249,7 +249,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op = { const_entry_body = invProof; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = true && (Options.boxed_definitions())}, + const_entry_boxed = true && (Flags.boxed_definitions())}, IsProof Lemma) in () diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 307968116..477beba4a 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -259,7 +259,7 @@ let default_relation_for_carrier ?(filter=fun _ -> true) a = [] -> Leibniz (Some a) | relation::tl -> if tl <> [] then - Options.if_warn msg_warning + Flags.if_warn msg_warning (str "There are several relations on the carrier \"" ++ pr_lconstr a ++ str "\". The relation " ++ prrelation relation ++ str " is chosen.") ; @@ -347,7 +347,7 @@ let (relation_to_obj, obj_to_relation)= match th.rel_sym with None -> old_relation.rel_sym | Some t -> Some t} in - Options.if_warn msg_warning + Flags.if_warn msg_warning (strbrk "The relation " ++ prrelation th' ++ strbrk " is redeclared. The new declaration" ++ (match th'.rel_refl with @@ -412,7 +412,7 @@ let morphism_table_add (m,c) = List.find (function mor -> mor.args = c.args && mor.output = c.output) old in - Options.if_warn msg_warning + Flags.if_warn msg_warning (strbrk "The morphism " ++ prmorphism m old_morph ++ strbrk " is redeclared. " ++ strbrk "The new declaration whose compatibility is proved by " ++ @@ -427,7 +427,7 @@ let default_morphism ?(filter=fun _ -> true) m = [] -> raise Not_found | m1::ml -> if ml <> [] then - Options.if_warn msg_warning + Flags.if_warn msg_warning (strbrk "There are several morphisms associated to \"" ++ pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++ strbrk " is randomly chosen."); @@ -689,7 +689,7 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = apply_to_rels mext quantifiers_rev |])); const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions()}, + const_entry_boxed = Flags.boxed_definitions()}, IsDefinition Definition)) ; mext in @@ -705,7 +705,7 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) = output = output_constr; lem = lem; morphism_theory = mmor })); - Options.if_verbose ppnl (pr_lconstr m ++ str " is registered as a morphism") + Flags.if_verbose ppnl (pr_lconstr m ++ str " is registered as a morphism") let error_cannot_unify_signature env k t t' = errorlabstrm "New Morphism" @@ -923,7 +923,7 @@ let new_morphism m signature id hook = Pfedit.start_proof id (Global, Proof Lemma) (Declare.clear_proofs (Global.named_context ())) lem hook; - Options.if_verbose msg (Printer.pr_open_subgoals ()); + Flags.if_verbose msg (Printer.pr_open_subgoals ()); end let morphism_hook _ ref = @@ -1043,7 +1043,7 @@ let int_add_relation id a aeq refl sym trans = a_quantifiers_rev); const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions()}, + const_entry_boxed = Flags.boxed_definitions()}, IsDefinition Definition) in let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in let xreflexive_relation_class = @@ -1060,14 +1060,14 @@ let int_add_relation id a aeq refl sym trans = Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() }, + const_entry_boxed = Flags.boxed_definitions() }, IsDefinition Definition) in let aeq_rel = { aeq_rel with rel_X_relation_class = current_constant id; rel_Xreflexive_relation_class = current_constant id_precise } in Lib.add_anonymous_leaf (relation_to_obj (aeq, aeq_rel)) ; - Options.if_verbose ppnl (pr_lconstr aeq ++ str " is registered as a relation"); + Flags.if_verbose ppnl (pr_lconstr aeq ++ str " is registered as a relation"); match trans with None -> () | Some trans -> @@ -1120,7 +1120,7 @@ let int_add_relation id a aeq refl sym trans = {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev; const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions()}, + const_entry_boxed = Flags.boxed_definitions()}, IsDefinition Definition) in let a_quantifiers_rev = @@ -1580,7 +1580,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = (fun i (_,_,mc) -> pr_new_goals i mc) res) | [he] -> he | he::_ -> - Options.if_warn msg_warning + Flags.if_warn msg_warning (strbrk "The application of the tactic is subject to one of " ++ strbrk "the following set of side conditions that the user needs " ++ strbrk "to prove:" ++ diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 09d9fe8d7..3211cc6cf 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -612,16 +612,11 @@ let rec intern_match_context_hyps sigma env lfun = function | (Hyp ((_,na) as locna,mp))::tl -> let ido, metas1, pat = intern_pattern sigma env lfun mp in let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in - let lfun' = name_cons na (option_cons ido lfun) in + let lfun' = name_cons na (Option.List.cons ido lfun) in lfun', metas1@metas2, Hyp (locna,pat)::hyps | [] -> lfun, [], [] (* Utilities *) -let rec filter_some = function - | None :: l -> filter_some l - | Some a :: l -> a :: filter_some l - | [] -> [] - let extract_names lrc = List.fold_right (fun ((loc,name),_) l -> @@ -833,7 +828,7 @@ and intern_tactic_seq ist = function and intern_tactic_fun ist (var,body) = let (l1,l2) = ist.ltacvars in - let lfun' = List.rev_append (filter_some var) l1 in + let lfun' = List.rev_append (Option.List.flatten var) l1 in (var,intern_tactic { ist with ltacvars = (lfun',l2) } body) and intern_tacarg strict ist = function @@ -872,7 +867,7 @@ and intern_match_rule ist = function let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in let ido,metas2,pat = intern_pattern sigma env lfun mp in let metas = list_uniquize (metas1@metas2) in - let ist' = { ist with ltacvars = (metas@(option_cons ido lfun'),l2) } in + let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl) | [] -> [] @@ -2635,18 +2630,18 @@ let make_absolute_name (loc,id) = kn let add_tacdef isrec tacl = -(* let isrec = if !Options.p1 then isrec else true in*) +(* let isrec = if !Flags.p1 then isrec else true in*) let rfun = List.map (fun ((loc,id as locid),_) -> (id,make_absolute_name locid)) tacl in let ist = {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in let gtacl = List.map (fun ((_,id),def) -> - (id,Options.with_option strict_check (intern_tactic ist) def)) + (id,Flags.with_option strict_check (intern_tactic ist) def)) tacl in let id0 = fst (List.hd rfun) in let _ = Lib.add_leaf id0 (inMD gtacl) in List.iter - (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined")) + (fun (id,_) -> Flags.if_verbose msgnl (pr_id id ++ str " is defined")) rfun (***************************************************************************) @@ -2655,7 +2650,7 @@ let add_tacdef isrec tacl = let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x let glob_tactic_env l env x = - Options.with_option strict_check + Flags.with_option strict_check (intern_tactic { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env }) x @@ -2674,7 +2669,7 @@ let _ = Auto.set_extern_interp interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); last_loc=dloc}) let _ = Auto.set_extern_intern_tac (fun l -> - Options.with_option strict_check + Flags.with_option strict_check (intern_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])})) let _ = Auto.set_extern_subst_tactic subst_tactic let _ = Dhyp.set_extern_interp eval_tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 782f2a4c1..f1f169394 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1298,7 +1298,7 @@ let unfold_all x gl = *) let check_unused_names names = - if names <> [] & Options.is_verbose () then + if names <> [] & Flags.is_verbose () then let s = if List.tl names = [] then " " else "s " in msg_warning (str"Unused introduction pattern" ++ str s ++ diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index b4b951f5f..89569453a 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -8,7 +8,7 @@ open Tacmach open Util -open Options +open Flags open Decl_kinds open Pp open Entries diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 832e444ca..5a1b8b8b4 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -26,7 +26,7 @@ let print_loc loc = let guill s = "\""^s^"\"" let where s = - if !Options.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) + if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *) @@ -138,7 +138,7 @@ let explain_exn_default = explain_exn_default_aux anomaly_string report let raise_if_debug e = - if !Options.debug then raise e + if !Flags.debug then raise e let _ = Tactic_debug.explain_logic_error := explain_exn_default diff --git a/toplevel/class.ml b/toplevel/class.ml index 436aa8409..f7d709480 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -247,7 +247,7 @@ let build_id_coercion idf_opt source = { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); const_entry_type = Some typ_f; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions()} in + const_entry_boxed = Flags.boxed_definitions()} in let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in ConstRef kn @@ -318,7 +318,7 @@ let try_add_new_coercion_with_source ref stre ~source = let add_coercion_hook stre ref = try_add_new_coercion ref stre; - Options.if_verbose message + Flags.if_verbose message (string_of_qualid (shortest_qualid_of_global Idset.empty ref) ^ " is now a coercion") diff --git a/toplevel/command.ml b/toplevel/command.ml index 99f9e3ed7..05ee50daf 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -10,7 +10,7 @@ open Pp open Util -open Options +open Flags open Term open Termops open Declarations @@ -132,7 +132,7 @@ let red_constant_entry bl ce = function let declare_global_definition ident ce local = let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in - if local = Local && Options.is_verbose() then + if local = Local && Flags.is_verbose() then msg_warning (pr_id ident ++ str" is declared as a global definition"); definition_message ident; ConstRef kn @@ -147,7 +147,7 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in definition_message ident; if Pfedit.refining () then - Options.if_verbose msg_warning + Flags.if_verbose msg_warning (str"Local definition " ++ pr_id ident ++ str" is not visible from current goals"); VarRef ident @@ -179,7 +179,7 @@ let declare_one_assumption is_coe (local,kind) c nl (_,ident) = let kn = declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in assumption_message ident; - if local=Local & Options.is_verbose () then + if local=Local & Flags.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ str" because it is at a global level"); ConstRef kn in @@ -214,7 +214,7 @@ let declare_one_elimination ind = { const_entry_body = c; const_entry_type = t; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() }, + const_entry_boxed = Flags.boxed_definitions() }, Decl_kinds.IsDefinition Definition) in definition_message id; kn @@ -283,7 +283,7 @@ let declare_eq_scheme sp = let cst_entry = {const_entry_body = eq_array.(i); const_entry_type = None; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } + const_entry_boxed = Flags.boxed_definitions() } in let cst_decl = (DefinitionEntry cst_entry),(IsDefinition Definition) in @@ -583,7 +583,7 @@ let prepare_inductive ntnl indl = ind_arity = ar; ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc }) indl in - List.fold_right option_cons ntnl [], indl + List.fold_right Option.List.cons ntnl [], indl let elim_flag = ref true @@ -785,7 +785,7 @@ let interp_recursive fixkind l boxed = (* Get interpretation metadatas *) let impls = compute_interning_datas env [] fixnames fixtypes in - let notations = List.fold_right option_cons ntnl [] in + let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = @@ -904,7 +904,7 @@ let build_induction_scheme lnamedepindsort = let ce = { const_entry_body = decl; const_entry_type = Some decltype; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } in + const_entry_boxed = Flags.boxed_definitions() } in let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in ConstRef kn :: lrecref in @@ -975,7 +975,7 @@ let build_combined_scheme name schemes = let ce = { const_entry_body = body; const_entry_type = Some typ; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } in + const_entry_boxed = Flags.boxed_definitions() } in let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in if_verbose ppnl (recursive_message Fixpoint None [snd name]) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 85c61d2d1..9f301d3a4 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -14,7 +14,7 @@ open Toplevel let (/) = Filename.concat -let set_debug () = Options.debug := true +let set_debug () = Flags.debug := true (* Loading of the ressource file. rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one @@ -41,7 +41,7 @@ let load_rcfile() = Vernac.load_vernac false !rcfile else () (* - Options.if_verbose + Flags.if_verbose mSGNL (str ("No .coqrc or .coqrc."^Coq_config.version^ " found. Skipping rcfile loading.")) *) @@ -49,7 +49,7 @@ let load_rcfile() = (msgnl (str"Load of rcfile failed."); raise e) else - Options.if_verbose msgnl (str"Skipping rcfile loading.") + Flags.if_verbose msgnl (str"Skipping rcfile loading.") let add_ml_include s = Mltop.add_ml_dir s @@ -99,7 +99,7 @@ let init_load_path () = let coqlib = (* variable COQLIB overrides the default library *) getenv_else "COQLIB" - (if Coq_config.local || !Options.boot then Coq_config.coqtop + (if Coq_config.local || !Flags.boot then Coq_config.coqtop else Coq_config.coqlib) in let user_contrib = coqlib/"user-contrib" in let dirs = "states" :: "contrib" :: dev in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7546ad310..affe7f4e4 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -11,7 +11,7 @@ open Pp open Util open System -open Options +open Flags open Names open Libnames open Nameops @@ -83,7 +83,7 @@ let add_load_vernacular verb s = let load_vernacular () = List.iter (fun (s,b) -> - if Options.do_translate () then + if Flags.do_translate () then with_option translate_file (Vernac.load_vernac b) s else Vernac.load_vernac b s) @@ -104,7 +104,7 @@ let require () = let compile_list = ref ([] : (bool * string) list) let add_compile verbose s = set_batch_mode (); - Options.make_silent true; + Flags.make_silent true; compile_list := (verbose,s) :: !compile_list let compile_files () = let init_state = States.freeze() in @@ -113,7 +113,7 @@ let compile_files () = (fun (v,f) -> States.unfreeze init_state; Constrintern.coqdoc_unfreeze coqdoc_init_state; - if Options.do_translate () then + if Flags.do_translate () then with_option translate_file (Vernac.compile v) f else Vernac.compile v f) @@ -155,7 +155,7 @@ let use_vm = ref false let set_vm_opt () = Vm.set_transp_values (not !boxed_val); - Options.set_boxed_definitions !boxed_def; + Flags.set_boxed_definitions !boxed_def; Vconv.set_use_vm !use_vm (*s Parsing of the command line. @@ -240,7 +240,7 @@ let parse_args is_ide = | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem | "-compile-verbose" :: [] -> usage () - | "-dont-load-proofs" :: rem -> Options.dont_load_proofs := true; parse rem + | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem | "-translate" :: rem -> make_translate true; parse rem @@ -250,13 +250,13 @@ let parse_args is_ide = | "-debug" :: rem -> set_debug (); parse rem | "-vm" :: rem -> use_vm := true; parse rem - | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem - | "-emacs-U" :: rem -> Options.print_emacs := true; - Options.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem + | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem + | "-emacs-U" :: rem -> Flags.print_emacs := true; + Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 - | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem + | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () @@ -274,15 +274,15 @@ let parse_args is_ide = | ("-m" | "--memory") :: rem -> memory_stat := true; parse rem - | "-xml" :: rem -> Options.xml_export := true; parse rem + | "-xml" :: rem -> Flags.xml_export := true; parse rem | "-output-context" :: rem -> output_context := true; parse rem - (* Scanned in Options! *) + (* Scanned in Flags. *) | "-v7" :: rem -> error "This version of Coq does not support v7 syntax" | "-v8" :: rem -> parse rem - | "-no-hash-consing" :: rem -> Options.hash_cons_proofs := false; parse rem + | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem | s :: rem -> if is_ide then begin diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index bb30c669f..e381fe753 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -10,7 +10,7 @@ open Pp open Util -open Options +open Flags open Names open Nameops open Term diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 7ebf3dfa9..d9a82a413 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -74,7 +74,7 @@ let (inTacticGrammar, outTacticGrammar) = let cons_production_parameter l = function | VTerm _ -> l - | VNonTerm (_,_,ido) -> option_cons ido l + | VNonTerm (_,_,ido) -> Option.List.cons ido l let rec tactic_notation_key = function | VTerm id :: _ -> id @@ -755,7 +755,7 @@ let find_precedence lev etyps symbols = error "The level of the leftmost non-terminal cannot be changed" | ETIdent | ETBigint | ETReference -> if lev = None then - Options.if_verbose msgnl (str "Setting notation at level 0") + Flags.if_verbose msgnl (str "Setting notation at level 0") else if lev <> Some 0 then error "A notation starting with an atomic expression must be at level 0"; @@ -773,7 +773,7 @@ let find_precedence lev etyps symbols = (match list_last symbols with Terminal _ -> true |_ -> false) -> if lev = None then - (Options.if_verbose msgnl (str "Setting notation at level 0"); 0) + (Flags.if_verbose msgnl (str "Setting notation at level 0"); 0) else Option.get lev | _ -> if lev = None then error "Cannot determine the level"; diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 43ab05aa8..71369f0ab 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -15,7 +15,7 @@ open Util open Pp -open Options +open Flags open System open Libobject open Library diff --git a/toplevel/record.ml b/toplevel/record.ml index 5cb8b2904..e80001d25 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -90,7 +90,7 @@ let warning_or_error coe indsp err = (pr_id fi ++ str " cannot be defined because it is not typable") in if coe then errorlabstrm "structure" st; - Options.if_verbose ppnl (hov 0 (str"Warning: " ++ st)) + Flags.if_verbose ppnl (hov 0 (str"Warning: " ++ st)) type field_status = | NoProjection of name @@ -171,10 +171,10 @@ let declare_projections indsp coers fields = const_entry_body = proj; const_entry_type = Some projtyp; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions() } in + const_entry_boxed = Flags.boxed_definitions() } in let k = (DefinitionEntry cie,IsDefinition StructureComponent) in let kn = declare_internal_constant fid k in - Options.if_verbose message (string_of_id fid ^" is defined"); + Flags.if_verbose message (string_of_id fid ^" is defined"); kn with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) in diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index aba5aeb27..f5044f1dc 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -10,7 +10,7 @@ open Pp open Util -open Options +open Flags open Cerrors open Vernac open Pcoq @@ -221,7 +221,7 @@ let make_emacs_prompt() = (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x) "" pending in let proof_info = if dpth >= 0 then string_of_int dpth else "0" in - if !Options.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " + if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " else "" (* A buffer to store the current command read on stdin. It is diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index eec73e390..75d1cdc99 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -13,7 +13,7 @@ open Pp open Lexer open Util -open Options +open Flags open System open Vernacexpr open Vernacinterp @@ -127,7 +127,7 @@ let rec vernac_com interpfun (loc,com) = (* end translator state *) (* coqdoc state *) let cds = Constrintern.coqdoc_freeze() in - if !Options.translate_file then + if !Flags.translate_file then begin let _,f = find_file_in_path (Library.get_load_paths ()) (make_suffix fname ".v") in @@ -137,13 +137,13 @@ let rec vernac_com interpfun (loc,com) = begin try read_vernac_file verbosely (make_suffix fname ".v"); - if !Options.translate_file then close_out !chan_translate; + if !Flags.translate_file then close_out !chan_translate; chan_translate := ch; Lexer.restore_com_state cs; Pp.comments := cl; Constrintern.coqdoc_unfreeze cds with e -> - if !Options.translate_file then close_out !chan_translate; + if !Flags.translate_file then close_out !chan_translate; chan_translate := ch; Lexer.restore_com_state cs; Pp.comments := cl; @@ -174,12 +174,12 @@ and vernac interpfun input = vernac_com interpfun (parse_phrase input) and read_vernac_file verbosely s = - Options.make_warn verbosely; + Flags.make_warn verbosely; let interpfun = if verbosely then Vernacentries.interp else - Options.silently Vernacentries.interp + Flags.silently Vernacentries.interp in let (in_chan, fname, input) = open_file_twice_if verbosely s in try @@ -213,22 +213,22 @@ let set_xml_end_library f = xml_end_library := f (* Load a vernac file. Errors are annotated with file and location *) let load_vernac verb file = chan_translate := - if !Options.translate_file then open_out (file^"8") else stdout; + if !Flags.translate_file then open_out (file^"8") else stdout; try read_vernac_file verb file; - if !Options.translate_file then close_out !chan_translate; + if !Flags.translate_file then close_out !chan_translate; with e -> - if !Options.translate_file then close_out !chan_translate; + if !Flags.translate_file then close_out !chan_translate; raise_with_file file e (* Compile a vernac file (f is assumed without .v suffix) *) let compile verbosely f = let ldir,long_f_dot_v = Library.start_library f in if !dump then dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); - if !Options.xml_export then !xml_start_library (); + if !Flags.xml_export then !xml_start_library (); let _ = load_vernac verbosely long_f_dot_v in if Pfedit.get_all_proof_names () <> [] then (message "Error: There are pending proofs"; exit 1); - if !Options.xml_export then !xml_end_library (); + if !Flags.xml_export then !xml_end_library (); Library.save_library_to ldir (long_f_dot_v ^ "o") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9cb2b26b7..cb9e95356 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -12,7 +12,7 @@ open Pp open Util -open Options +open Flags open Names open Entries open Nameops @@ -330,7 +330,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook = let vernac_end_proof = function | Admitted -> admit () | Proved (is_opaque,idopt) -> - if not !Options.print_emacs then if_verbose show_script (); + if not !Flags.print_emacs then if_verbose show_script (); match idopt with | None -> save_named is_opaque | Some ((_,id),None) -> save_anonymous is_opaque id @@ -537,7 +537,7 @@ let vernac_solve n tcom b = (* in case a strict subtree was completed, go back to the top of the prooftree *) if subtree_solved () then begin - Options.if_verbose msgnl (str "Subgoal proved"); + Flags.if_verbose msgnl (str "Subgoal proved"); make_focus 0; reset_top_of_script () end; @@ -773,8 +773,8 @@ let _ = { optsync = true; optname = "raw printing"; optkey = (SecondaryTable ("Printing","All")); - optread = (fun () -> !Options.raw_print); - optwrite = (fun b -> Options.raw_print := b) } + optread = (fun () -> !Flags.raw_print); + optwrite = (fun b -> Flags.raw_print := b) } let _ = declare_bool_option @@ -789,8 +789,8 @@ let _ = { optsync = true; optname = "use of boxed definitions"; optkey = (SecondaryTable ("Boxed","Definitions")); - optread = Options.boxed_definitions; - optwrite = (fun b -> Options.set_boxed_definitions b) } + optread = Flags.boxed_definitions; + optwrite = (fun b -> Flags.set_boxed_definitions b) } let _ = declare_bool_option @@ -813,8 +813,8 @@ let _ = { optsync=false; optkey=SecondaryTable("Hyps","Limit"); optname="the hypotheses limit"; - optread=Options.print_hyps_limit; - optwrite=Options.set_print_hyps_limit } + optread=Flags.print_hyps_limit; + optwrite=Flags.set_print_hyps_limit } let _ = declare_int_option diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index fc9ed778a..7d99fe721 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -64,7 +64,7 @@ let call (opn,converted_args) = | Drop -> raise Drop | ProtectedLoop -> raise ProtectedLoop | e -> - if !Options.debug then + if !Flags.debug then msgnl (str"Vernac Interpreter " ++ str !loc); raise e diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 4a200591e..c7a9774e0 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -10,7 +10,7 @@ (* $Id$ *) -open Options +open Flags open Pp open Util open System |