| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Remove unused optional "predicative" argument. |  Guillaume Melquiond | 2016-08-10 |
| | | |||
| * | 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 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |