aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.ml
Commit message (Expand)AuthorAge
* 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-06-21 08:01:49 +0000