diff options
| author | Maxime Dénès | 2018-01-18 17:55:54 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-18 17:55:54 +0100 |
| commit | f26bf29cfe6fb154400f3a1305b86b34ad88e0e2 (patch) | |
| tree | 2123a95066b6097bfb5105abf46835f31f939780 /dev/include | |
| parent | 4d8903c06fd9fd2aca793da8bb55448906347a8c (diff) | |
| parent | 7b9f83224e13b21fcb5bd1b3742f52070c3299e4 (diff) | |
Merge PR #6448: Cleanup and add debug printers a bit
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 0d34595f4f..b982f4c9fa 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;; |