aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/proofBlockDelimiter.ml
Commit message (Collapse)AuthorAge
* [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
| | | | | | | | | | `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select`
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
| | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
|
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
| | | | | | | | | | | | Virtually all classifications of vernacular commands (the STM classifier, "filtered commands", "navigation commands", etc.) were broken in presence of control vernaculars like Time, Timeout, Fail. Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac Debug in CoqIDE. This change introduces a type separation between vernacular controls and vernacular commands, together with an "under_control" combinator.
* [plugins] Prepare plugin API for functional handling of state.Gravatar Emilio Jesus Gallego Arias2017-11-19
| | | | | | | | To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
* [stm] Move interpretation state to VernacentriesGravatar Emilio Jesus Gallego Arias2017-10-17
| | | | | We still don't thread the state there, but this is a start of the needed infrastructure.
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
| | | | | | | | | | | | | | We make the Stm API functional over an opaque `doc` type. This allows to have a much better picture of what the toplevel is doing; now almost all users of STM private data are marked by typing. For now only, the API is functional; a PR switching the internals should come soon thou; however we must first fix some initialization bugs. Due to some users, we modify `feedback` internally to include a "document id" field; we don't expose this change in the IDE protocol yet.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* [stm] Fix record field name clash.Gravatar Emilio Jesus Gallego Arias2016-10-18
| | | | | | | | | | PR#173 introduced a record field name clash in `stm.mli`, with duplicate fields `start/stop` for the types `focus` and `static_block_declaration`. We fix by renaming the younger ones (as to minimize code incompatibilities), but other options are possible/could be preferred, however they would be quite more invasive so I think they should be postponed for the day the Stm API is cleaned up.
* DocumentationGravatar Enrico Tassi2016-06-07
|
* Error box detection run only on errorGravatar Enrico Tassi2016-06-06
| | | | | Advantage: 0 cost if no error occurs Disadvantage: a box *must* end with the error absorbing command
* STM: proof block detection for indentationGravatar Enrico Tassi2016-06-06
|
* STM: proof block detection for par:Gravatar Enrico Tassi2016-06-06
| | | | | "par: tac" is a terminator, if it fails we can admit all focused goals and continue.
* STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-23 13:26:04 +0000