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 | |
| 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.
| -rw-r--r-- | library/library.mllib | 2 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 | ||||
| -rw-r--r-- | vernac/printmod.ml (renamed from printing/printmod.ml) | 0 | ||||
| -rw-r--r-- | vernac/printmod.mli (renamed from printing/printmod.mli) | 0 | ||||
| -rw-r--r-- | vernac/states.ml (renamed from library/states.ml) | 0 | ||||
| -rw-r--r-- | vernac/states.mli (renamed from library/states.mli) | 1 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 2 |
7 files changed, 2 insertions, 4 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 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 diff --git a/printing/printmod.ml b/vernac/printmod.ml index 9beac17546..9beac17546 100644 --- a/printing/printmod.ml +++ b/vernac/printmod.ml diff --git a/printing/printmod.mli b/vernac/printmod.mli index c7f056063b..c7f056063b 100644 --- a/printing/printmod.mli +++ b/vernac/printmod.mli diff --git a/library/states.ml b/vernac/states.ml index b6904263df..b6904263df 100644 --- a/library/states.ml +++ b/vernac/states.ml diff --git a/library/states.mli b/vernac/states.mli index fb50a1a8bd..51db83ca03 100644 --- a/library/states.mli +++ b/vernac/states.mli @@ -30,4 +30,3 @@ val replace_lib : state -> Lib.frozen -> state state of the whole system as it was before applying [f] *) val with_state_protection : ('a -> 'b) -> 'a -> 'b - diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 23dde0dd29..085e2e35bc 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -1,6 +1,8 @@ Vernacexpr Attributes Pvernac +States +Printmod Declaremods G_vernac G_proofs |