aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofview.ml
Commit message (Expand)AuthorAge
...
* Revert "Naming main goal "Main""Gravatar Hugo Herbelin2014-10-16
* Refactoring proofview: make the definition of the logic monad polymorphic.Gravatar Arnaud Spiwack2014-10-16
* Grab Existential Variables: restore the goal order from v8.4.Gravatar Arnaud Spiwack2014-10-16
* Proofview: cleanup: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-16
* Put evars remaining after a tactic on the shelf.Gravatar Arnaud Spiwack2014-10-16
* Refine: proper scoping of the future goals.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove [advance] from the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview: remove unused [refresh_sigma] compatibility primitive.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove most of the API (make [Goal.goal] concrete).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
* Move the handling of the principal evar from refine to evd.Gravatar Arnaud Spiwack2014-10-16
* Move the handling a new evars from the [Proofview.Refine] module to [Evd].Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Gravatar Arnaud Spiwack2014-10-16
* Proofview: small optimisation/simplification.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
* Naming main goal "Main"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
* A few Global.env removed.Gravatar Hugo Herbelin2014-10-04
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
* 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
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* No plural for only one non existing focused goal.Gravatar Hugo Herbelin2014-09-12
* Fix source of initial 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
* Ensuring the invariant that hypotheses and named context of the environment ofGravatar Pierre-Marie Pédrot2014-09-04
* 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
* Using goal-tactics to interpret arguments to idtac.Gravatar Pierre-Marie Pédrot2014-09-04
* Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."Gravatar Pierre-Marie Pédrot2014-09-04
* Putting back normalized goals when entering them.Gravatar Pierre-Marie Pédrot2014-09-03
* Simplification of the tclCHECKINTERRUPT tactic.Gravatar Pierre-Marie Pédrot2014-08-28
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
* New primitive allowing to modify refine handles.Gravatar Pierre-Marie Pédrot2014-08-19
* Hypotheses in [Proofview.Goal.enter] were not normalised.Gravatar Arnaud Spiwack2014-08-07
* Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Gravatar Arnaud Spiwack2014-08-05
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
* Add primtive [num_goal] to Proofview.Gravatar Arnaud Spiwack2014-08-01
* Adding a tclBREAK primitive to the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-04 23:24:59 +0000