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 /vernac/comProgramFixpoint.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 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions