diff options
| author | Gaëtan Gilbert | 2019-10-28 16:48:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-31 14:42:54 +0100 |
| commit | 215b7e43cba768bfc82914718b159a22797f9d2b (patch) | |
| tree | 706f80870c1d18af5e920c518a3e7f09df3d6f69 /vernac/vernac.mllib | |
| parent | ae1eb22a1365a6f477fc328eabf821fd346b5f0b (diff) | |
Move prettyp (Print implementation) to vernac/
Diffstat (limited to 'vernac/vernac.mllib')
| -rw-r--r-- | vernac/vernac.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 102da20257..7563b4a5d5 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -10,6 +10,7 @@ Locality Egramml Vernacextend Ppvernac +Prettyp Proof_using Egramcoq Metasyntax |