diff options
| author |  Jason Gross <jgross@mit.edu> | 2015-06-23 10:12:41 +0200 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-05 22:09:39 -0400 |
| commit | 9ff2c9d8d042c9989b6a8138c308398c49ae116f (patch) | |
| tree | ab6abf0403a4db27fef257393795111284da20ae /library/declaremods.mli | |
| 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/declaremods.mli')
| -rw-r--r-- | library/declaremods.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 2b440c087..3917fe8d6 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 |