aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.ml
Commit message (Expand)AuthorAge
* Adjust EConstr.cmp_constructors for relaxed constructor cumulativityGravatar Gaëtan Gilbert2018-03-09
* Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
* Statically enforce that ULub is only between levels.Gravatar Gaëtan Gilbert2018-03-09
* Option for messing with inference of irrelevant constraintsGravatar Gaëtan Gilbert2018-03-09
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Define EConstr version of [push_rec_types].Gravatar Cyprien Mangin2018-01-19
* [econstr] Add a couple of new API functions.Gravatar Emilio Jesus Gallego Arias2017-12-13
* [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-12-13
* Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
* Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Normalizing universes before performing term comparison.Gravatar Pierre-Marie Pédrot2017-09-08
* Using EConstr equality check in unification.Gravatar Pierre-Marie Pédrot2017-09-08
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...Gravatar Maxime Dénès2017-06-06
|\
| * Using EConstr and more invariants in record.ml.Gravatar Hugo Herbelin2017-05-31
* | tactics cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
|/
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Exporting some functions of vars.ml as functions operating on EConstr.Gravatar Hugo Herbelin2017-05-19
* In EConstr, defining some "cast" functions earlier.Gravatar Hugo Herbelin2017-05-19
* Moving "sym" on "eq" type to lib/util.ml.Gravatar Hugo Herbelin2017-05-19
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Restore a fast path in EConstr instance normalization.Gravatar Pierre-Marie Pédrot2017-04-01
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
* Ensuring proper cast invariants in EConstr.kind.Gravatar Pierre-Marie Pédrot2017-03-31
* Revert "Specially crafted EConstr.kind to be more efficient."Gravatar Pierre-Marie Pédrot2017-03-31
* Specially crafted EConstr.kind to be more efficient.Gravatar Pierre-Marie Pédrot2017-03-30
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
* Missing API in EConstr.Gravatar Enrico Tassi2017-02-14
* Moving evar-normalization functions to EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Introducing a new EConstr.t type to perform the nf_evar operation on demand.Gravatar Pierre-Marie Pédrot2016-11-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 23:35:31 +0000