aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/sigma.ml
Commit message (Expand)AuthorAge
* Remove unused optional "predicative" argument.Gravatar Guillaume Melquiond2016-08-10
* Allowing to attach location to universes in UState.Gravatar Pierre-Marie Pédrot2016-02-19
* Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
* Removing some goal unsafeness in inductive schemes.Gravatar Pierre-Marie Pédrot2015-10-29
* Removing some unsafe uses of monotonicity.Gravatar Pierre-Marie Pédrot2015-10-19
* Adding a notion of monotonous evarmap.Gravatar Pierre-Marie Pédrot2015-10-18