aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.mli
Commit message (Expand)AuthorAge
* Export Proofview.undefined as "unsafe" primitive.Gravatar Hugo Herbelin2018-03-27
* Adding informative variant of shelve_unifiable returning set of shelved evars.Gravatar Hugo Herbelin2018-03-27
* Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.Gravatar Hugo Herbelin2018-03-08
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Proofview: V82.tactic option to not normalize evarsGravatar Enrico Tassi2018-03-04
* | proofview: debug API to print a goalGravatar Enrico Tassi2018-03-04
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* | proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
|/
* [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
* Proofview: enter_one: add __LOC__ argument to get relevant error msgGravatar Enrico Tassi2018-01-31
* [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
* [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* [proofs] Remove circular dependency from Proofview to Goal.Gravatar Emilio Jesus Gallego Arias2017-07-19
* Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...Gravatar Maxime Dénès2017-07-07
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * In enter_one, not having exactly one goal is a fatal error of the monad.Gravatar Hugo Herbelin2017-06-23
|/
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-16 22:59:59 +0000