diff options
| author | Emilio Jesus Gallego Arias | 2019-06-09 21:35:43 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-25 18:25:46 +0200 |
| commit | 9419b85a053f155781db788cfbdfe36308ee0dd1 (patch) | |
| tree | 77fb7e5d062c3bfbc7d27d4517ebf182ada0813c /kernel/nativelambda.ml | |
| parent | 7dfcb0f7c817e66280ab37b6c653b5596a16c249 (diff) | |
[lemmas] Move `Stack` out of Lemmas.
We move the stack of open lemmas from `Lemmas` to `Vernacstate`. The
`Lemmas` module doesn't deal with stacked proofs, so the stack can be
moved to to the proper place; this reduces the size of the API.
Note that `Lemmas` API is still quite imperative, it would be great if
we would return some more information on close proof, for example
about the global environment parts that were modified.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions