aboutsummaryrefslogtreecommitdiff
path: root/proofs/proofview.mli
AgeCommit message (Expand)Author
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-12Make sure the goals on the shelve are identified as goal and unresolvable for...Arnaud Spiwack
2014-12-07Exporting store of goals so that new_evar in convert, intro, etc. canHugo Herbelin
2014-11-30Adding missing unsafe primitives to Proofview.Pierre-Marie Pédrot
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
2014-11-01Info: do not record info trace unless needed.Arnaud Spiwack
2014-11-01Info: print a name for the primitive tactics in [Proofview].Arnaud Spiwack
2014-11-01Add [Info] command.Arnaud Spiwack
2014-11-01An API for info traces.Arnaud Spiwack
2014-10-22Specializing tclBREAK so that it can choose the return exception in casePierre-Marie Pédrot
2014-10-22Proofview: documentation and re-ordering.Arnaud Spiwack
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-10-22Make names in [Proofview_monad] more uniform.Arnaud Spiwack
2014-10-22Proofview: move [list_goto] to the [CList] module.Arnaud Spiwack
2014-10-22Proofview: remove a redundant primitive.Arnaud Spiwack
2014-10-22Proofview: move more functions to the Unsafe module.Arnaud Spiwack
2014-10-22Proofview: split [V82] module into [Unsafe] and [V82].Arnaud Spiwack
2014-10-22Proofview.mli: no more reference to Goal.goal.Arnaud Spiwack
2014-10-22Remove unused functions for side effects.Arnaud Spiwack
2014-10-16Refactoring proofview: make the definition of the logic monad polymorphic.Arnaud Spiwack
2014-10-16Put evars remaining after a tactic on the shelf.Arnaud Spiwack
2014-10-16Proofview: remove unused [refresh_sigma] compatibility primitive.Arnaud Spiwack
2014-10-16Expose Proofview.Refine.with_type in the API.Arnaud Spiwack
2014-10-16Proofview.Refine: remove the handle type, and simplify the API.Arnaud Spiwack
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
2014-10-09Added support for having one subgoal inheriting the name of its father in Ref...Hugo Herbelin
2014-10-09A version of convert_concl and convert_hyp in new proof engine.Hugo Herbelin
2014-10-06Make tclEFFECTS also update the env in the proof monadEnrico Tassi
2014-09-27Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Pierre-Marie Pédrot
2014-09-26Adding a tclNEWGOALS primitive.Pierre-Marie Pédrot
2014-09-18Fixing strange evarmap leak in goals.Pierre-Marie Pédrot
2014-09-15Fix timing of evar-normalisation of goals in [Ftactic.nf_enter].Arnaud Spiwack
2014-09-12While we don't have a clean alternative to Clenvtac, add a primitiveMatthieu Sozeau
2014-09-12Add syntax [id]: to apply tactic to goal named id.Hugo Herbelin
2014-09-12No plural for only one non existing focused goal.Hugo Herbelin
2014-09-08Display number of available goals in "incorrect number of goals" error message.Arnaud Spiwack
2014-09-08Add a tactic [revgoals] to reverse the list of focused goals.Arnaud Spiwack
2014-09-06Renaming goal-entering functions.Pierre-Marie Pédrot
2014-09-05At last a working clearbody!Pierre-Marie Pédrot
2014-09-04Proofview refiner is now type-safe by default.Pierre-Marie Pédrot
2014-09-04Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Pierre-Marie Pédrot
2014-09-04Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Pierre-Marie Pédrot
2014-08-28Simplification of the tclCHECKINTERRUPT tactic.Pierre-Marie Pédrot
2014-08-28Cleaning and documenting a bit the Proofview.Refine module.Pierre-Marie Pédrot
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-21Removing unused parts of the Goal.sensitive monad.Pierre-Marie Pédrot
2014-08-19New primitive allowing to modify refine handles.Pierre-Marie Pédrot
2014-08-05Adding a [make] primitive to the NonLogical monad.Pierre-Marie Pédrot
2014-08-05Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Arnaud Spiwack
2014-08-04Cleaning of the new implementation of the tactic monad.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 02:55:10 +0000