aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.mli
Commit message (Expand)AuthorAge
* 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
|/
* Exporting some functions of vars.ml as functions operating on EConstr.Gravatar Hugo Herbelin2017-05-19
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* 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
* 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 11:00:31 +0000