aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printing.mllib
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-30 16:43:14 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-30 16:43:14 +0200
commitb75f714c025b51ed8b4db15bfce99df2d6ae7c41 (patch)
tree4c25d6cbc0d6f62450c15ebdda03a3ada717c8e1 /printing/printing.mllib
parentb1714dcc7df330df92a935f202964a1e73e44652 (diff)
parent7c62654a4a1c0711ebdd492193bb8b7bd0e4f1fb (diff)
Merge PR #7558: [api] Make `vernac/` self-contained.
Diffstat (limited to 'printing/printing.mllib')
-rw-r--r--printing/printing.mllib1
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/printing.mllib b/printing/printing.mllib
index 86b68d8fb..b69d8a9ef 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -4,4 +4,3 @@ Ppconstr
Printer
Printmod
Prettyp
-Ppvernac