diff options
-rw-r--r-- | contrib/funind/indfun_common.ml | 7 | ||||
-rw-r--r-- | contrib/subtac/subtac.ml | 13 | ||||
-rw-r--r-- | interp/constrintern.ml | 16 | ||||
-rw-r--r-- | interp/dumpglob.ml | 72 | ||||
-rw-r--r-- | lib/flags.ml | 9 | ||||
-rw-r--r-- | lib/flags.mli | 5 | ||||
-rw-r--r-- | scripts/coqc.ml | 2 | ||||
-rw-r--r-- | tactics/auto.ml | 2 | ||||
-rw-r--r-- | tools/coqdoc/cdglobals.ml | 7 | ||||
-rw-r--r-- | tools/coqdoc/main.ml | 8 | ||||
-rw-r--r-- | toplevel/coqtop.ml | 10 | ||||
-rw-r--r-- | toplevel/usage.ml | 3 | ||||
-rw-r--r-- | toplevel/vernac.ml | 12 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 48 |
14 files changed, 115 insertions, 99 deletions
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 4010b49d5..a3c169b7e 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -238,20 +238,19 @@ let with_full_print f a = and old_strict_implicit_args = Impargs.is_strict_implicit_args () and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in - let old_dump = !Flags.dump in Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; Impargs.make_contextual_implicit_args false; Impargs.make_contextual_implicit_args false; - Flags.dump := false; + Dumpglob.pause (); try let res = f a in 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; Flags.raw_print := old_rawprint; - Flags.dump := old_dump; + Dumpglob.continue (); res with | e -> @@ -259,7 +258,7 @@ let with_full_print f a = Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; - Flags.dump := old_dump; + Dumpglob.continue (); raise e diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 71aa7e99e..fbb4589b8 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -120,7 +120,7 @@ let dump_variable lid = () let vernac_assumption env isevars kind l nl = let global = fst kind = Global in List.iter (fun (is_coe,(idl,c)) -> - if !Flags.dump then + if Dumpglob.dump () then List.iter (fun lid -> if global then dump_definition lid "ax" else dump_variable lid) idl; @@ -140,7 +140,7 @@ let subtac (loc, command) = match command with | VernacDefinition (defkind, (_, id as lid), expr, hook) -> check_fresh lid; - dump_definition lid "def"; + if Dumpglob.dump () then dump_definition lid "def"; (match expr with | ProveBody (bl, t) -> if Lib.is_modtype () then @@ -153,12 +153,12 @@ let subtac (loc, command) = | VernacFixpoint (l, b) -> List.iter (fun ((lid, _, _, _, _), _) -> check_fresh lid; - dump_definition lid "fix") l; + if Dumpglob.dump () then dump_definition lid "fix") l; let _ = trace (str "Building fixpoint") in ignore(Subtac_command.build_recursive l b) | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) -> - if !Flags.dump then dump_definition id "prf"; + if Dumpglob.dump () then dump_definition id "prf"; if not(Pfedit.refining ()) then if lettop then errorlabstrm "Subtac_command.StartProof" @@ -173,11 +173,12 @@ let subtac (loc, command) = vernac_assumption env isevars stre l nl | VernacInstance (glob, sup, is, props, pri) -> - if !Flags.dump then dump_constraint "inst" is; + if Dumpglob.dump () then dump_constraint "inst" is; ignore(Subtac_classes.new_instance ~global:glob sup is props pri) | VernacCoFixpoint (l, b) -> - List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l; + if Dumpglob.dump () then + List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l; ignore(Subtac_command.build_corecursive l b) (*| VernacEndProof e -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d802770f0..fccfb1bf3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -252,7 +252,7 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) = let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args = let ntn,args = contract_notation ntn args in let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in - if !Flags.dump then Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df; + if Dumpglob.dump () then Dumpglob.dump_notation_location (Topconstr.ntn_loc loc args ntn) df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in subst_aconstr_in_rawconstr loc intern subst ([],env) c @@ -334,10 +334,10 @@ let check_no_explicitation l = let intern_qualid loc qid intern env args = try match Nametab.extended_locate qid with | TrueGlobal ref -> - Dumpglob.add_glob loc ref; + if Dumpglob.dump() then Dumpglob.add_glob loc ref; RRef (loc, ref), args | SyntacticDef sp -> - Dumpglob.add_glob_kn loc sp; + if Dumpglob.dump() then Dumpglob.add_glob_kn loc sp; let (ids,c) = Syntax_def.search_syntactic_definition loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments loc; @@ -567,7 +567,7 @@ let find_constructor ref f aliases pats scopes = let v = Environ.constant_value (Global.env()) cst in unf (global_of_constr v) | ConstructRef cstr -> - Dumpglob.add_glob loc r; + if Dumpglob.dump() then Dumpglob.add_glob loc r; cstr, [], pats | _ -> raise Not_found in unf r @@ -618,7 +618,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat = | CPatNotation (loc, ntn, args) -> let ntn,args = contract_pat_notation ntn args in let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in - if !Flags.dump then Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df; + if Dumpglob.dump () then Dumpglob.dump_notation_location (Topconstr.patntn_loc loc args ntn) df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes c @@ -627,7 +627,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat = let a = alias_of aliases in let (c,df) = Notation.interp_prim_token_cases_pattern loc p a (tmp_scope,scopes) in - if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df; + if Dumpglob.dump () then Dumpglob.dump_notation_location (fst (unloc loc)) df; (ids,[subst,c]) | CPatDelimiters (loc, key, e) -> intern_pat (find_delimiters_scope loc key::scopes) aliases None e @@ -687,7 +687,7 @@ let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function | Anonymous -> env | Name id -> check_hidden_implicit_parameters id lvar; - Dumpglob.dump_binding loc id; + if Dumpglob.dump() then Dumpglob.dump_binding loc id; (Idset.add id ids,tmpsc,scopes) let intern_typeclass_binders intern_type lvar env bl = @@ -887,7 +887,7 @@ let internalise sigma globalenv env allow_patvar lvar c = intern_notation intern env loc ntn args | CPrim (loc, p) -> let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in - if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df; + if Dumpglob.dump () then Dumpglob.dump_notation_location (fst (unloc loc)) df; c | CDelimiters (loc, key, e) -> intern (ids,None,find_delimiters_scope loc key::scopes) e diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 84117fafa..b8121af86 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -16,7 +16,7 @@ let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> h let glob_file = ref Pervasives.stdout let open_glob_file f = - glob_file := Pervasives.open_out(f ^ ".glob") + glob_file := Pervasives.open_out f let close_glob_file () = Pervasives.close_out !glob_file @@ -24,10 +24,29 @@ let close_glob_file () = let dump_string s = Pervasives.output_string !glob_file s +type glob_output_t = + | None + | StdOut + | MultFiles + | File of string + +let glob_output = ref MultFiles + +let dump () = !glob_output != None + +let noglob () = glob_output := None + +let dump_to_stdout () = glob_output := StdOut + +let multi_dump () = !glob_output = MultFiles + +let dump_into_file f = glob_output := File f; open_glob_file f + +let previous_state = ref MultFiles +let pause () = previous_state := !glob_output +let continue () = glob_output := !previous_state -(**********************************************************************) -(* Dump of globalization (to be used by coqdoc) *) let token_number = ref 0 let last_pos = ref 0 @@ -117,25 +136,21 @@ let add_glob_gen loc sp lib_dp ty = dump_ref loc filepath modpath ident ty let add_glob loc ref = - let sp = Nametab.sp_of_global ref in - let lib_dp = Lib.library_part ref in - let ty = type_of_global_ref ref in - add_glob_gen loc sp lib_dp ty + if loc <> Util.dummy_loc then + let sp = Nametab.sp_of_global ref in + let lib_dp = Lib.library_part ref in + let ty = type_of_global_ref ref in + add_glob_gen loc sp lib_dp ty -let add_glob loc ref = - if !Flags.dump && loc <> Util.dummy_loc then add_glob loc ref - let mp_of_kn kn = let mp,sec,l = Names.repr_kn kn in Names.MPdot (mp,l) let add_glob_kn loc kn = - let sp = Nametab.sp_of_syntactic_definition kn in - let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in - add_glob_gen loc sp lib_dp "syndef" - -let add_glob_kn loc ref = - if !Flags.dump && loc <> Util.dummy_loc then add_glob_kn loc ref + if loc <> Util.dummy_loc then + let sp = Nametab.sp_of_syntactic_definition kn in + let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in + add_glob_gen loc sp lib_dp "syndef" let add_local loc id = () (* let mod_dp,id = repr_path sp in *) @@ -189,23 +204,20 @@ let dump_local_binder b sec ty = | Topconstr.LocalRawDef _ -> () let dump_modref loc mp ty = - if !Flags.dump then - let (dp, l) = Lib.split_modpath mp in - let fp = Names.string_of_dirpath dp in - let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in - dump_string (Printf.sprintf "R%d %s %s %s %s\n" - (fst (Util.unloc loc)) fp mp "<>" ty) + let (dp, l) = Lib.split_modpath mp in + let fp = Names.string_of_dirpath dp in + let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in + dump_string (Printf.sprintf "R%d %s %s %s %s\n" + (fst (Util.unloc loc)) fp mp "<>" ty) let dump_moddef loc mp ty = - if !Flags.dump then - let (dp, l) = Lib.split_modpath mp in - let mp = Names.string_of_dirpath (Names.make_dirpath l) in - dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp) + let (dp, l) = Lib.split_modpath mp in + let mp = Names.string_of_dirpath (Names.make_dirpath l) in + dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp) let dump_libref loc dp ty = - if !Flags.dump then - dump_string (Printf.sprintf "R%d %s <> <> %s\n" - (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty) + dump_string (Printf.sprintf "R%d %s <> <> %s\n" + (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty) let dump_notation_location pos ((path,df),sc) = let rec next growing = @@ -218,7 +230,7 @@ let dump_notation_location pos ((path,df),sc) = let loc = next (pos >= !last_pos) in last_pos := pos; let path = Names.string_of_dirpath path in - let _sc = match sc with Some sc -> " "^sc | None -> "" in + let _sc = match sc with Some sc -> " "^sc | _ -> "" in dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df) diff --git a/lib/flags.ml b/lib/flags.ml index f2ab87b4b..4743345de 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -82,18 +82,13 @@ let unsafe_set = ref Stringset.empty let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set let is_unsafe s = Stringset.mem s !unsafe_set -(* Dump of globalization (to be used by coqdoc) *) - -let noglob = ref false -let dump = ref false - -(* Flags.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 -(* Flags.for external tools *) +(* Flags for external tools *) let subst_command_placeholder s t = let buff = Buffer.create (String.length s + String.length t) in diff --git a/lib/flags.mli b/lib/flags.mli index 4cab30381..8c16e5b85 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -57,11 +57,6 @@ val print_hyps_limit : unit -> int option val add_unsafe : string -> unit val is_unsafe : string -> bool -(* Dump of globalization (to be used by coqdoc) *) - -val noglob : bool ref -val dump : bool ref - (* Options for the virtual machine *) val set_boxed_definitions : bool -> unit diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 84f12049a..6915d60bc 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -141,7 +141,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" as o) :: rem -> + |"-init-file" | "-dump-glob" as o) :: rem -> begin match rem with | s :: rem' -> parse (cfiles,s::o::args) rem' diff --git a/tactics/auto.ml b/tactics/auto.ml index 1c3e2ce08..6641289eb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -478,7 +478,7 @@ let add_hints local dbnames0 h = (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ str "to an evaluable reference.") in - if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr; + if Dumpglob.dump () then Dumpglob.add_glob (loc_of_reference r) gr; (gr,r') in add_unfolds (List.map f lhints) local dbnames | HintsConstructors lqid -> diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 44b9bd3ce..3339b1dba 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -32,6 +32,13 @@ let open_out_file f = let close_out_file () = close_out !out_channel +type glob_source_t = + | NoGlob + | DotGlob + | GlobFile of string + +let glob_source = ref DotGlob + let header_trailer = ref true let header_file = ref "" let header_file_spec = ref false diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 7466a6ba1..d9384adc4 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -50,6 +50,7 @@ let usage () = prerr_endline " --tex <file> consider <file> as a .tex file"; prerr_endline " -p <string> insert <string> in LaTeX preamble"; prerr_endline " --files-from <file> read file names to process in <file>"; + prerr_endline " --glob-from <file> read globalization information from <file>"; prerr_endline " --quiet quiet mode (default)"; prerr_endline " --verbose verbose mode"; prerr_endline " --no-externals no links to Coq standard library"; @@ -300,7 +301,7 @@ let parse () = | "-R" :: ([] | [_]) -> usage () | ("-glob-from" | "--glob-from") :: f :: rem -> - obsolete "glob-from"; parse_rec rem + glob_source := GlobFile f; parse_rec rem | ("-glob-from" | "--glob-from") :: [] -> usage () | ("--no-externals" | "-no-externals" | "-noexternals") :: rem -> @@ -436,7 +437,10 @@ let produce_document l = Filename.concat !output_dir "coqdoc.sty" else "coqdoc.sty" in copy src dst); - let l = List.map read_glob l in + (match !Cdglobals.glob_source with + | NoGlob -> () + | DotGlob -> ignore (List.map read_glob l) + | GlobFile f -> ignore (Index.read_glob f)); List.iter index_module l; match !out_to with | StdOut -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7e92b804c..1a856d477 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -240,8 +240,12 @@ let parse_args is_ide = | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem | "-load-vernac-object" :: [] -> usage () - | "-dump-glob" :: _ :: rem -> warning "option -dumpglob is obsolete"; parse rem - | ("-no-glob" | "-noglob") :: rem -> Flags.noglob := true; parse rem + | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); parse rem + (* À ne pas documenter : l'option 'stdout' n'étant + éventuellement utile que pour le debugging... *) + | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; parse rem + | "-dump-glob" :: [] -> usage () + | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); parse rem | "-require" :: f :: rem -> add_require f; parse rem | "-require" :: [] -> usage () @@ -265,7 +269,7 @@ let parse_args is_ide = | "-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 - + | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 124ce0593..417a496f8 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -57,7 +57,8 @@ let print_usage_channel co command = -batch batch mode (exits just after arguments parsing) -boot boot mode (implies -q and -batch) -emacs tells Coq it is executed under Emacs - -no-glob f do not dump globalizations + -noglob f do not dump globalizations + -dump-glob f dump globalizations in file f (to be used by coqdoc) -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes) -impredicative-set set sort Set impredicative -dont-load-proofs don't load opaque proofs in memory diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d3c556147..ae35b0fa1 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -226,18 +226,16 @@ let load_vernac verb file = (* 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 - let dumpstate = !Flags.dump in - if not !Flags.noglob then - (Flags.dump := true; - Dumpglob.open_glob_file f; - Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n")); + if Dumpglob.multi_dump () then + Dumpglob.open_glob_file (f ^ ".glob"); + if Dumpglob.dump () then + Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"); 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 !Flags.xml_export then !xml_end_library (); - if !Flags.dump then Dumpglob.close_glob_file (); - Flags.dump := dumpstate; + if Dumpglob.multi_dump () then Dumpglob.close_glob_file (); Library.save_library_to ldir (long_f_dot_v ^ "o") diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 246e35dad..65b36edb6 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -277,7 +277,7 @@ let print_located_module r = let global_with_alias r = let gr = global_with_alias r in - if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr; + if Dumpglob.dump () then Dumpglob.add_glob (loc_of_reference r) gr; gr (**********) @@ -308,7 +308,7 @@ let start_proof_and_print k l hook = if !pcoq <> None then (Option.get !pcoq).start_proof () let vernac_definition (local,_,_ as k) (loc,id as lid) def hook = - if !Flags.dump then Dumpglob.dump_definition lid false "def"; + if Dumpglob.dump () then Dumpglob.dump_definition lid false "def"; (match def with | ProveBody (bl,t) -> (* local binders, typ *) if Lib.is_modtype () then @@ -327,7 +327,7 @@ let vernac_definition (local,_,_ as k) (loc,id as lid) def hook = declare_definition id k bl red_option c typ_opt hook) let vernac_start_proof kind l lettop hook = - if !Flags.dump then + if Dumpglob.dump () then List.iter (fun (id, _) -> match id with | Some lid -> Dumpglob.dump_definition lid false "prf" @@ -366,14 +366,14 @@ let vernac_exact_proof c = let vernac_assumption kind l nl= let global = fst kind = Global in List.iter (fun (is_coe,(idl,c)) -> - if !Flags.dump then + if Dumpglob.dump () then List.iter (fun lid -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl; declare_assumption idl is_coe kind [] c false false nl) l let vernac_inductive f indl = - if !Flags.dump then + if Dumpglob.dump () then List.iter (fun ((lid, _, _, cstrs), _) -> Dumpglob.dump_definition lid false"ind"; List.iter (fun (_, (lid, _)) -> @@ -382,12 +382,12 @@ let vernac_inductive f indl = build_mutual indl f let vernac_fixpoint l b = - if !Flags.dump then + if Dumpglob.dump () then List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; build_recursive l b let vernac_cofixpoint l b = - if !Flags.dump then + if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; build_corecursive l b @@ -421,7 +421,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o = Modintern.interp_modtype Modintern.interp_modexpr id binders_ast (Some mty_ast_o) None in - if !Flags.dump then Dumpglob.dump_moddef loc mp "mod"; + if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is declared"); Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export @@ -441,7 +441,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = let mp = Declaremods.start_module Modintern.interp_modtype export id binders_ast mty_ast_o in - if !Flags.dump then Dumpglob.dump_moddef loc mp "mod"; + if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Interactive Module "^ string_of_id id ^" started") ; List.iter @@ -461,7 +461,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = Modintern.interp_modtype Modintern.interp_modexpr id binders_ast mty_ast_o mexpr_ast_o in - if !Flags.dump then Dumpglob.dump_moddef loc mp "mod"; + if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is defined"); Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) @@ -469,7 +469,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o = let vernac_end_module export (loc,id) = let mp = Declaremods.end_module id in - if !Flags.dump then Dumpglob.dump_modref loc mp "mod"; + if Dumpglob.dump () then Dumpglob.dump_modref loc mp "mod"; if_verbose message ("Module "^ string_of_id id ^" is defined") ; Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export @@ -487,7 +487,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast ([],[]) in let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in - if !Flags.dump then Dumpglob.dump_moddef loc mp "modtype"; + if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "modtype"; if_verbose message ("Interactive Module Type "^ string_of_id id ^" started"); List.iter @@ -506,14 +506,14 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o = else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_modtype id binders_ast base_mty in - if !Flags.dump then Dumpglob.dump_moddef loc mp "modtype"; + if Dumpglob.dump () then Dumpglob.dump_moddef loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype id in - if !Flags.dump then Dumpglob.dump_modref loc mp "modtype"; + if Dumpglob.dump () then Dumpglob.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") @@ -532,7 +532,7 @@ let vernac_record struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) | Some (_,id as lid) -> - if !Flags.dump then Dumpglob.dump_definition lid false "constr"; id in + if Dumpglob.dump () then Dumpglob.dump_definition lid false "constr"; id in let sigma = Evd.empty in let env = Global.env() in let s = interp_constr sigma env sort in @@ -541,7 +541,7 @@ let vernac_record struc binders sort nameopt cfs = | Sort s -> s | _ -> user_err_loc (constr_loc sort,"definition_structure", str "Sort expected.") in - if !Flags.dump then ( + if Dumpglob.dump () then ( Dumpglob.dump_definition (snd struc) false "rec"; List.iter (fun (_, x) -> match x with @@ -553,11 +553,11 @@ let vernac_record struc binders sort nameopt cfs = let vernac_begin_section (_, id as lid) = check_no_pending_proofs (); - if !Flags.dump then Dumpglob.dump_definition lid true "sec"; + if Dumpglob.dump () then Dumpglob.dump_definition lid true "sec"; Lib.open_section id let vernac_end_section (loc, id) = - if !Flags.dump then + if Dumpglob.dump () then Dumpglob.dump_reference loc (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section id @@ -576,7 +576,7 @@ let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in let modrefl = List.map Library.try_locate_qualified_library qidl in (* let modrefl = List.map (fun qid -> let (dp, _) = (Library.try_locate_qualified_library qid) in dp) qidl in *) - if !Flags.dump then + if Dumpglob.dump () then List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl (List.map fst modrefl); Library.require_library_from_dirpath modrefl import @@ -597,21 +597,21 @@ let vernac_identity_coercion stre id qids qidt = (* Type classes *) let vernac_class id par ar sup props = - if !Flags.dump then ( + if Dumpglob.dump () then ( Dumpglob.dump_definition id false "class"; List.iter (fun (lid, _, _) -> Dumpglob.dump_definition lid false "meth") props); Classes.new_class id par ar sup props let vernac_instance glob sup inst props pri = - if !Flags.dump then Dumpglob.dump_constraint inst false "inst"; + if Dumpglob.dump () then Dumpglob.dump_constraint inst false "inst"; ignore(Classes.new_instance ~global:glob sup inst props pri) let vernac_context l = - if !Flags.dump then List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l; + if Dumpglob.dump () then List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l; Classes.context l let vernac_declare_instance id = - if !Flags.dump then Dumpglob.dump_definition id false "inst"; + if Dumpglob.dump () then Dumpglob.dump_definition id false "inst"; Classes.declare_instance false id (***********) @@ -746,7 +746,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef let vernac_hints = Auto.add_hints let vernac_syntactic_definition lid = - if !Flags.dump then Dumpglob.dump_definition lid false "syndef"; + if Dumpglob.dump () then Dumpglob.dump_definition lid false "syndef"; Command.syntax_definition (snd lid) let vernac_declare_implicits local r = function |