index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
/
eConstr.ml
Commit message (
Expand
)
Author
Age
*
Restore a fast path in EConstr instance normalization.
Pierre-Marie Pédrot
2017-04-01
*
Using delayed universe instances in EConstr.
Pierre-Marie Pédrot
2017-04-01
*
Actually exporting delayed universes in the EConstr implementation.
Pierre-Marie Pédrot
2017-04-01
*
Make the Constr.kind_of_term type parametric in sorts and universes.
Pierre-Marie Pédrot
2017-03-31
*
Ensuring proper cast invariants in EConstr.kind.
Pierre-Marie Pédrot
2017-03-31
*
Revert "Specially crafted EConstr.kind to be more efficient."
Pierre-Marie Pédrot
2017-03-31
*
Specially crafted EConstr.kind to be more efficient.
Pierre-Marie Pédrot
2017-03-30
*
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
*
Missing API in EConstr.
Enrico Tassi
2017-02-14
*
Moving evar-normalization functions to EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Namegen primitives now apply on evar constrs.
Pierre-Marie Pédrot
2017-02-14
*
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
*
Contradiction API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Equality API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Tactics API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Clenv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
Making judgment type generic over the type of inner constrs.
Pierre-Marie Pédrot
2017-02-14
*
Introducing a new EConstr.t type to perform the nf_evar operation on demand.
Pierre-Marie Pédrot
2016-11-08