diff options
| author | Gaëtan Gilbert | 2020-07-01 12:23:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 12:23:39 +0200 |
| commit | b017e302f69f20fc4fc3d4088a305194f6c387fa (patch) | |
| tree | e38585c69863280e0a62037b0e615cc0a584f76c /printing/printing.mllib | |
| parent | 144d121ad9a5b2aead25f9365021a9753a835e12 (diff) | |
| parent | b0169fc220ced87d094177575c0dae76d8d87a50 (diff) | |
Merge PR #12504: [states] Move States to vernac
Reviewed-by: SkySkimmer
Ack-by: maximedenes
Diffstat (limited to 'printing/printing.mllib')
| -rw-r--r-- | printing/printing.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/printing/printing.mllib b/printing/printing.mllib index 5b5b6590a4..39e160706b 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -3,4 +3,3 @@ Pputils Ppconstr Proof_diffs Printer -Printmod |