diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 4 | ||||
| -rw-r--r-- | library/goptions.ml | 2 | ||||
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/library.ml | 10 | ||||
| -rw-r--r-- | library/nametab.ml | 4 |
5 files changed, 12 insertions, 12 deletions
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 |