Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Making Evd independent from Namegen. | Pierre-Marie Pédrot | 2017-02-14 |
| | |||
* | Remove unused optional "predicative" argument. | Guillaume Melquiond | 2016-08-10 |
| | |||
* | Adding a bit of documentation in the mli. | Pierre-Marie Pédrot | 2016-06-09 |
| | |||
* | Allowing to attach location to universes in UState. | Pierre-Marie Pédrot | 2016-02-19 |
| | |||
* | Monotonizing the Evarutil module. | Pierre-Marie Pédrot | 2016-02-15 |
| | | | | | Some functions were left in the old paradigm because they are only used by the unification algorithms, so they are not worthwhile to change for now. | ||
* | Removing some goal unsafeness in inductive schemes. | Pierre-Marie Pédrot | 2015-10-29 |
| | |||
* | Removing some unsafe uses of monotonicity. | Pierre-Marie Pédrot | 2015-10-19 |
| | |||
* | Adding a notion of monotonous evarmap. | Pierre-Marie Pédrot | 2015-10-18 |