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 /library/library.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 'library/library.mllib')
| -rw-r--r-- | library/library.mllib | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/library/library.mllib b/library/library.mllib index a6188f7661..cdc131cfab 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,7 +5,5 @@ Summary Nametab Global Lib -States -Kindops Goptions Coqlib |