aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.mli
Commit message (Expand)AuthorAge
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
| * Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
| * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
|/
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
* 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
* Proofview: extensions for backtracking eautoGravatar Matthieu Sozeau2016-06-16
* Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
* Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\
| * Fix a typo in proofs/proofview.mli.Gravatar Cyprien Mangin2016-06-14
| * Add goal range selectors.Gravatar Cyprien Mangin2016-06-14
* | STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06
|/
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20