diff options
| author | ppedrot | 2013-05-12 15:33:27 +0000 |
|---|---|---|
| committer | ppedrot | 2013-05-12 15:33:27 +0000 |
| commit | 9a9a8ab4c2a07aa8faa04f50d6250930220b5be5 (patch) | |
| tree | e6cbd9730c892dc6386b9c1c68d53489b478f6f8 /dev | |
| parent | 0e69a26eadeabf5987aacdac57cd6a5b90b0cdc8 (diff) | |
Added a generic notion of hook. Hooks are functions to be set
exactly once at runtime, often to reduce the mutual dependency of
modules. This module permits to track them more easily.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/printers.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 01b44f1484..e7c3b1a1b9 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -1,5 +1,6 @@ Coq_config +Hook Int Option Store |