aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/keys.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Remove keys for evar and meta, since they cannot occur.Gravatar Guillaume Melquiond2016-01-02
* | Remove some useless type declarations.Gravatar Guillaume Melquiond2016-01-02
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
* First version of keyed subterm selection in unification.Gravatar Matthieu Sozeau2014-09-27