aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/refine.mli
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
* Turn the default behaviour of the refine primitive into the safe one.Gravatar Pierre-Marie Pédrot2017-06-13
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Removing unused warnings.Gravatar Pierre-Marie Pédrot2017-05-19
* Generalizing the refine primitive so as to accept tactic arguments.Gravatar Pierre-Marie Pédrot2017-05-03
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
| * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
|/
* Adding variants enter_one and refine_one which assume that exactly oneGravatar Hugo Herbelin2016-09-16
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
* Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 22:02:38 +0000