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.ml | |
| 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.ml')
| -rw-r--r-- | library/declaremods.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index f3f734aa0..dcd63c769 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 |