diff options
| author | Emilio Jesus Gallego Arias | 2020-06-12 04:37:50 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 13:12:01 +0200 |
| commit | e260c203fa74a587bd78b2803c8ee046ff3df20a (patch) | |
| tree | 57b6a7e60443f3bd8344d18b9bba158759c7c669 /printing/printing.mllib | |
| parent | bffe3e8dcbb6019b30d32081f0b56eba30bf8be7 (diff) | |
[states] Move States to vernac
We continue to push state layers upwards, in preparation of a
functional vernacular interpretation.
Now we move `States` and `Printmod` which messes with the global
state as to temporarily create envs with modules.
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 |