diff options
| author | ppedrot | 2013-08-01 18:53:49 +0000 |
|---|---|---|
| committer | ppedrot | 2013-08-01 18:53:49 +0000 |
| commit | 505284b57bff03d22d55c31df11733fdd687f602 (patch) | |
| tree | 354d7a28ec65df47bdc4c764abeb330d18fc5a55 /intf | |
| parent | 88f8c20e3f55e8548d1f33b3407e68fb7dfb8317 (diff) | |
Added a Print Debug GC command that displays the current state of
the OCaml GC, as indicated by [Gc.stat].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16651 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index bbb68689c3..d19857ee1c 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -45,6 +45,7 @@ type printable = | PrintNamespace of DirPath.t | PrintMLLoadPath | PrintMLModules + | PrintDebugGC | PrintName of reference or_by_notation | PrintGraph | PrintClasses |