aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.mli
Commit message (Expand)AuthorAge
* Adding an unshelve tactical.Gravatar Pierre-Marie Pédrot2015-12-09
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Make sure the goals on the shelve are identified as goal and unresolvable for...Gravatar Arnaud Spiwack2014-12-12
* Exporting store of goals so that new_evar in convert, intro, etc. canGravatar Hugo Herbelin2014-12-07
* Adding missing unsafe primitives to Proofview.Gravatar Pierre-Marie Pédrot2014-11-30
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
* Info: do not record info trace unless needed.Gravatar Arnaud Spiwack2014-11-01
* Info: print a name for the primitive tactics in [Proofview].Gravatar Arnaud Spiwack2014-11-01
* Add [Info] command.Gravatar Arnaud Spiwack2014-11-01
* An API for info traces.Gravatar Arnaud Spiwack2014-11-01
* Specializing tclBREAK so that it can choose the return exception in caseGravatar Pierre-Marie Pédrot2014-10-22
* Proofview: documentation and re-ordering.Gravatar Arnaud Spiwack2014-10-22
* Split [Proofview] into a file where the basic operations on the state are def...Gravatar Arnaud Spiwack2014-10-22
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
* Proofview: move [list_goto] to the [CList] module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: remove a redundant primitive.Gravatar Arnaud Spiwack2014-10-22
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Proofview.mli: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-22
* Remove unused functions for side effects.Gravatar Arnaud Spiwack2014-10-22
* Refactoring proofview: make the definition of the logic monad polymorphic.Gravatar Arnaud Spiwack2014-10-16
* Put evars remaining after a tactic on the shelf.Gravatar Arnaud Spiwack2014-10-16
* Proofview: remove unused [refresh_sigma] compatibility primitive.Gravatar Arnaud Spiwack2014-10-16
* Expose Proofview.Refine.with_type in the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* Adding a tactic which fails if one of the goals under focus is dependent in a...Gravatar Hugo Herbelin2014-10-13
* Added support for having one subgoal inheriting the name of its father in Ref...Gravatar Hugo Herbelin2014-10-09
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
* Make tclEFFECTS also update the env in the proof monadGravatar Enrico Tassi2014-10-06
* Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Gravatar Pierre-Marie Pédrot2014-09-27
* Adding a tclNEWGOALS primitive.Gravatar Pierre-Marie Pédrot2014-09-26
* Fixing strange evarmap leak in goals.Gravatar Pierre-Marie Pédrot2014-09-18
* Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Gravatar Arnaud Spiwack2014-09-15
* While we don't have a clean alternative to Clenvtac, add a primitiveGravatar Matthieu Sozeau2014-09-12
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
* No plural for only one non existing focused goal.Gravatar Hugo Herbelin2014-09-12
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
* Simplification of the tclCHECKINTERRUPT tactic.Gravatar Pierre-Marie Pédrot2014-08-28
* Cleaning and documenting a bit the Proofview.Refine module.Gravatar Pierre-Marie Pédrot2014-08-28
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 23:03:02 +0000