diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-16 22:31:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-12 16:29:11 +0200 |
| commit | 4ed9c7ad75a7f09d723bdfce6f7dd086c60e0601 (patch) | |
| tree | d322952b91456f1f2811d7758fd8fef690405577 /vernac/vernac.mllib | |
| parent | 3a7d9fcafedc4987d0748a8717b2b012a779de39 (diff) | |
[stm] Move main parsing entry point to the STM.
Mainly due to notations, proof modes and plugins, parsing in Coq is
stateful, so we expose a state-aware parsing API in the STM.
This is a first move to unify all the parsing entry points in the Stm
and the toplevel, and allows STM clients to control their input stream
properly. This greatly helps for instance, with whole-document
parsing.
This commit supersedes PR#204.
Diffstat (limited to 'vernac/vernac.mllib')
0 files changed, 0 insertions, 0 deletions