diff options
| -rw-r--r-- | ltac/ltac.mllib | 1 | ||||
| -rw-r--r-- | ltac/pptactic.ml (renamed from printing/pptactic.ml) | 0 | ||||
| -rw-r--r-- | ltac/pptactic.mli (renamed from printing/pptactic.mli) | 0 | ||||
| -rw-r--r-- | ltac/pptacticsig.mli (renamed from printing/pptacticsig.mli) | 0 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 |
5 files changed, 1 insertions, 1 deletions
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 1fe29b115..b9b63be3a 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -1,3 +1,4 @@ +Pptactic Pltac Taccoerce Tacsubst diff --git a/printing/pptactic.ml b/ltac/pptactic.ml index a4222ae2c..a4222ae2c 100644 --- a/printing/pptactic.ml +++ b/ltac/pptactic.ml diff --git a/printing/pptactic.mli b/ltac/pptactic.mli index 86e3ea548..86e3ea548 100644 --- a/printing/pptactic.mli +++ b/ltac/pptactic.mli diff --git a/printing/pptacticsig.mli b/ltac/pptacticsig.mli index 455cc1be1..455cc1be1 100644 --- a/printing/pptacticsig.mli +++ b/ltac/pptacticsig.mli diff --git a/printing/printing.mllib b/printing/printing.mllib index bc8f0750e..b0141b6d3 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -3,7 +3,6 @@ Pputils Ppannotation Ppconstr Printer -Pptactic Printmod Prettyp Ppvernac |