Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Bump year in headers. | Pierre-Marie Pédrot | 2017-07-04 |
| | |||
* | Clean up universes of constants and inductives | Amin Timany | 2017-06-16 |
| | |||
* | Fix bugs and add an option for cumulativity | Amin Timany | 2017-06-16 |
| | |||
* | Using UInfoInd for universes in inductive types | Amin Timany | 2017-06-16 |
| | | | | | | | | | It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. | ||
* | Extend definition of inductives to include subtyping info | Amin Timany | 2017-06-16 |
| | |||
* | Renaming local_binder into local_binder_expr. | Hugo Herbelin | 2017-03-24 |
| | | | | This is a bit long, but it is to keep a symmetry with constr_expr. | ||
* | [stm] Break stm/toplevel dependency loop. | Emilio Jesus Gallego Arias | 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. |