aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/funind/indfun_common.ml7
-rw-r--r--contrib/subtac/subtac.ml13
-rw-r--r--interp/constrintern.ml16
-rw-r--r--interp/dumpglob.ml72
-rw-r--r--lib/flags.ml9
-rw-r--r--lib/flags.mli5
-rw-r--r--scripts/coqc.ml2
-rw-r--r--tactics/auto.ml2
-rw-r--r--tools/coqdoc/cdglobals.ml7
-rw-r--r--tools/coqdoc/main.ml8
-rw-r--r--toplevel/coqtop.ml10
-rw-r--r--toplevel/usage.ml3
-rw-r--r--toplevel/vernac.ml12
-rw-r--r--toplevel/vernacentries.ml48
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 06:05:14 +0000