aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
* 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
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
* Only using filtered hyps in Goal.enter.Gravatar Pierre-Marie Pédrot2014-09-04
* Ensuring the invariant that hypotheses and named context of the environment ofGravatar Pierre-Marie Pédrot2014-09-04
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
* Fix: shelve_unifiable did not work modulo evar instantiation.Gravatar Arnaud Spiwack2014-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
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Simplification of the tclCHECKINTERRUPT tactic.Gravatar Pierre-Marie Pédrot2014-08-28
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-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
* Move UnsatisfiableConstraints to a pretype error.Gravatar Matthieu Sozeau2014-08-22
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
* Removing a use of Goal.refine.Gravatar Pierre-Marie Pédrot2014-08-19
* New primitive allowing to modify refine handles.Gravatar Pierre-Marie Pédrot2014-08-19
* Improving error message when applying rewrite to an expression which is not a...Gravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* More self-contained code for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Removing unused Refiner.tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
* Hypotheses in [Proofview.Goal.enter] were not normalised.Gravatar Arnaud Spiwack2014-08-07
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
* Adding a [make] primitive to the NonLogical monad.Gravatar Pierre-Marie Pédrot2014-08-05
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Goal: API to get the solution of a goalGravatar Enrico Tassi2014-08-05
* Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].Gravatar Arnaud Spiwack2014-08-05
* Some comments in the interface of Proofview_monad.Gravatar Arnaud Spiwack2014-08-04
* Cleaning the new implementation of the tactic monad continued.Gravatar Arnaud Spiwack2014-08-04
* 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
* Clean outdated comment in Proofview.Notations.Gravatar Arnaud Spiwack2014-08-01
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31
* Adding a tclBREAK primitive to the tactic monad.Gravatar Pierre-Marie Pédrot2014-07-28
* Add a tactic [swap i j] to swap the position of goals [i] and [j].Gravatar Arnaud Spiwack2014-07-25
* Adds a cycle tactic to reorder goals in a loop.Gravatar Arnaud Spiwack2014-07-25
* Small reorganisation in proof.ml.Gravatar Arnaud Spiwack2014-07-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 06:06:30 +0000