aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/keys.mli
Commit message (Expand)AuthorAge
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-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
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* 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