diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 20:21:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-01 19:34:58 +0200 |
| commit | fa1782e05eeb6f18871d26cc43670d35ed73bf23 (patch) | |
| tree | a182392b3f511f6a2f8f8899239802cf3d310532 /interp/dumpglob.mli | |
| parent | 66e52c88076ba830c8c8b3cf8e4bb77959fb7843 (diff) | |
[dumpglob] Move dumpglob-specific data to dumpglob.
The whole business of cst_kind is fishy tho, it seems to me that it
should be removed from the libobject path.
Diffstat (limited to 'interp/dumpglob.mli')
| -rw-r--r-- | interp/dumpglob.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 18955985a0..e0308b8afc 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -45,3 +45,6 @@ val dump_constraint : Names.lname -> bool -> string -> unit val dump_string : string -> unit val type_of_global_ref : Names.GlobRef.t -> string + +(** Registration of constant information *) +val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit |