Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | [option] Remove support for non-synchronous options. | 2017-05-24 | |
| | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers. | ||
* | Merge PR#627: Obligations shrinking: shrink abstraction too | 2017-05-20 | |
|\ | |||
* | | Uniformity of style for selecting plural or not; spacing for comma. | 2017-05-13 | |
| | | |||
| * | Obligations shrinking: shrink abstraction too | 2017-05-11 | |
|/ | |||
* | More consistent writing of de Bruijn. | 2017-05-01 | |
| | |||
* | Merge branch 'trunk' into pr379 | 2017-03-24 | |
| | |||
* | Make Obligations see fix_exn | 2017-02-15 | |
| | |||
* | [stm] Break stm/toplevel dependency loop. | 2017-02-15 | |
Currently, the STM, vernac interpretation, and the toplevel are intertwined in a mutual dependency that needs to be resolved using imperative callbacks. This is problematic for a few reasons, in particular it makes the interpretation of commands that affect the document quite intricate. As a first step, we split the `toplevel/` directory into two: "pure" vernac interpretation is moved to the `vernac/` directory, on which the STM relies. Test suite passes, and only one command seems to be disabled with this approach, "Show Script" which is to my understanding obsolete. Subsequent commits will fix this and refine some of the invariants that are not needed anymore. |