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.ml | |
| 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.ml')
| -rw-r--r-- | interp/dumpglob.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 53baf137cf..482303d935 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -104,13 +104,20 @@ let type_of_logical_kind = function | Corollary -> "thm") | IsPrimitive -> "prim" + +(** Data associated to global parameters and constants *) + +let csttab = Summary.ref (Names.Cmap.empty : logical_kind Names.Cmap.t) ~name:"CONSTANT" +let add_constant_kind kn k = csttab := Names.Cmap.add kn k !csttab +let constant_kind kn = Names.Cmap.find kn !csttab + let type_of_global_ref gr = if Typeclasses.is_class gr then "class" else match gr with | Globnames.ConstRef cst -> - type_of_logical_kind (Decls.constant_kind cst) + type_of_logical_kind (constant_kind cst) | Globnames.VarRef v -> "var" ^ type_of_logical_kind (Decls.variable_kind v) | Globnames.IndRef ind -> |