Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge branch 'master' into econstr | 2017-04-07 | |
|\ | |||
| * | Merge PR#508: Optimize pending evars | 2017-04-06 | |
| |\ | |||
* | | | Merge branch 'trunk' into pr379 | 2017-04-04 | |
|\| | | |||
* | | | Merge branch 'trunk' into pr379 | 2017-03-24 | |
| | | | |||
| * | | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | 2017-03-24 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. | ||
| * | | Unifying standard "constr_level" names for constructors of local_binder_expr. | 2017-03-24 | |
| | | | | | | | | | | | | RawLocal -> CLocal | ||
| * | | "Standardizing" the name LocalPatten into LocalRawPattern. | 2017-03-24 | |
|/ / | |||
| * | Ensuring static invariants about handling of pending evars in Pretyping. | 2017-03-23 | |
|/ | | | | | | All functions where actually called with the second argument of the pending problem being the current evar map. We simply remove this useless and error-prone second component. | ||
* | Merge branch 'v8.6' | 2017-02-22 | |
| | |||
* | [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. |