diff options
| author | Jason Gross | 2015-06-23 10:12:41 +0200 |
|---|---|---|
| committer | Jason Gross | 2016-06-05 22:09:39 -0400 |
| commit | 9ff2c9d8d042c9989b6a8138c308398c49ae116f (patch) | |
| tree | ab6abf0403a4db27fef257393795111284da20ae /library | |
| parent | 45748e4efae8630cc13b0199dfcc9803341e8cd8 (diff) | |
LtacProf for Coq trunk
This add LtacProfiling. Much of the code was written by Tobias Tebbi
(@tebbi), and Paul A. Steckler was invaluable in porting the code to Coq
v8.5 and Coq trunk.
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 6 | ||||
| -rw-r--r-- | library/declaremods.mli | 3 |
2 files changed, 9 insertions, 0 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index f3f734aa09..dcd63c7691 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -897,7 +897,13 @@ let start_library dir = Lib.start_compilation dir mp; Lib.add_frozen_state () +let end_library_hook = ref ignore +let append_end_library_hook f = + let old_f = !end_library_hook in + end_library_hook := fun () -> old_f(); f () + let end_library ?except dir = + !end_library_hook(); let oname = Lib.end_compilation_checks dir in let mp,cenv,ast = Global.export ?except dir in let prefix, lib_stack = Lib.end_compilation oname in diff --git a/library/declaremods.mli b/library/declaremods.mli index 2b440c087a..3917fe8d64 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -90,6 +90,9 @@ val end_library : ?except:Future.UUIDSet.t -> library_name -> Safe_typing.compiled_library * library_objects * Safe_typing.native_library +(** append a function to be executed at end_library *) +val append_end_library_hook : (unit -> unit) -> unit + (** [really_import_module mp] opens the module [mp] (in a Caml sense). It modifies Nametab and performs the [open_object] function for every object of the module. Raises [Not_found] when [mp] is unknown |