aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.mli
Commit message (Expand)AuthorAge
* Add a bit of doc to EConstr.decompose_lam*Gravatar Gaëtan Gilbert2018-06-08
* Split off Universes functions about substitutions and constraintsGravatar Gaëtan Gilbert2018-05-17
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Gravatar Pierre-Marie Pédrot2018-04-13
|\
| * [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
* | [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
|/
* Delayed weak constraints for cumulative inductive types.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
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* | Add a comment on EConstr.to_constr regarding evar-freeness.Gravatar Pierre-Marie Pédrot2018-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
* Merge PR #6368: [api] Remove yet another type alias.Gravatar Maxime Dénès2017-12-11
|\
| * [api] Remove yet another type alias.Gravatar Emilio Jesus Gallego Arias2017-12-09
* | 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] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* 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-22 11:54:37 +0000