diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-16 10:58:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-22 16:36:32 +0100 |
| commit | 87cbd64254f33439882156d9a297a6a2f6886057 (patch) | |
| tree | 8ffc7a81a0018c0a7d91c24871c84da00bea4996 /dev/include | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
Cleanup debug printers a bit, add generated mli.
Diffstat (limited to 'dev/include')
| -rw-r--r-- | dev/include | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/include b/dev/include index 0d34595f4..b982f4c9f 100644 --- a/dev/include +++ b/dev/include @@ -36,7 +36,6 @@ #install_printer (* constraints *) ppconstraints;; #install_printer (* univ constraints *) ppuniverseconstraints;; #install_printer (* universe *) ppuni;; -#install_printer (* universes *) ppuniverse;; #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; |