diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-15 13:33:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-15 13:34:18 +0200 |
| commit | 21dc493a93853525c5d9c33c0c7558909ce5e79d (patch) | |
| tree | 811b3c254c279f5e5b97003c05eac65c4ba76d7f | |
| parent | 404a8c619f76c572aec65f413baf087a374b37c3 (diff) | |
Moving Ltac printers to ltac/ folder.
| -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 |