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 /ltac/ltac.mllib | |
| parent | 404a8c619f76c572aec65f413baf087a374b37c3 (diff) | |
Moving Ltac printers to ltac/ folder.
Diffstat (limited to 'ltac/ltac.mllib')
| -rw-r--r-- | ltac/ltac.mllib | 1 |
1 files changed, 1 insertions, 0 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 |