index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
eConstr.ml
Age
Commit message (
Expand
)
Author
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-01-19
Define EConstr version of [push_rec_types].
Cyprien Mangin
2017-12-13
[econstr] Add a couple of new API functions.
Emilio Jesus Gallego Arias
2017-12-13
[econstr] Cleanup in `vernac/classes.ml`.
Emilio Jesus Gallego Arias
2017-12-06
Fix #6323: stronger restrict universe context vs abstract.
Gaëtan Gilbert
2017-12-01
Cleanup API for registering universe binders.
Matthieu Sozeau
2017-11-22
[api] Deprecate Term destructors, move to Constr
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-09-08
Normalizing universes before performing term comparison.
Pierre-Marie Pédrot
2017-09-08
Using EConstr equality check in unification.
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-06-06
Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...
Maxime Dénès
2017-05-31
Using EConstr and more invariants in record.ml.
Hugo Herbelin
2017-05-29
tactics cleanup: remove constr_of_global calls
Matthieu Sozeau
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-19
Exporting some functions of vars.ml as functions operating on EConstr.
Hugo Herbelin
2017-05-19
In EConstr, defining some "cast" functions earlier.
Hugo Herbelin
2017-05-19
Moving "sym" on "eq" type to lib/util.ml.
Hugo Herbelin
2017-04-27
Remove unused [open] statements
Gaetan Gilbert
2017-04-01
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-03-31
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-30
Specially crafted EConstr.kind to be more efficient.
Pierre-Marie Pédrot
2017-02-14
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
2016-11-08
Introducing a new EConstr.t type to perform the nf_evar operation on demand.
Pierre-Marie Pédrot
[prev]
