Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Update headers following #6543. | 2018-02-27 | |
| | |||
* | Remove query-in-IDE warning. | 2017-12-27 | |
| | | | | | | | I don't understand what is wrong with putting a query in a script running in the IDE. It is typically needed when giving demos, and that sounds like a ligitimate use case. By the way, we do it ourselves every year during the demo at CoqPL... | ||
* | Separate vernac controls and regular commands. | 2017-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. | ||
* | Bump year in headers. | 2017-07-04 | |
| | |||
* | [stm] Port the toplevel to the STM. | 2017-04-12 | |
- We clean-up `Vernac` and make it use the STM API. - Now functions in `Vernac` for use in the toplevel and compiler take an starting `Stateid.t`. - Duplicated `Stm.interp` entry point is removed. - The XML protocol call `interp` is disabled. |