aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/inferCumulativity.ml
Commit message (Expand)AuthorAge
* Merge PR #6769: Split closure cache and remove whd_bothGravatar Maxime Dénès2018-03-09
|\
| * Pass the constant cache as a separate argument in kernel reduction.Gravatar Pierre-Marie Pédrot2018-03-04
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
* Fix reduction flags in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
* inferCumulativity: add comment to explain [if not is_arity].Gravatar Gaëtan Gilbert2018-02-11
* Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11