aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refine.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Maxime Dénès2017-06-01
* Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
* Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
* Adding variants enter_one and refine_one which assume that exactly oneGravatar Hugo Herbelin2016-09-16
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-02
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20