| Commit message (Expand) | Author | Age |
* | Add syntax [id]: to apply tactic to goal named id. | Hugo Herbelin | 2014-09-12 |
* | Use evar name to print goal. | Hugo Herbelin | 2014-09-12 |
* | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | 2014-09-12 |
* | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin | 2014-09-12 |
* | No plural for only one non existing focused goal. | Hugo Herbelin | 2014-09-12 |
* | Fix source of initial goal. | Hugo Herbelin | 2014-09-12 |
* | A step towards better differentiating when w_unify is used for subterm | Hugo Herbelin | 2014-09-10 |
* | Fixing localisation of tactic errors (my mistake in himsg.ml essentially). | Hugo Herbelin | 2014-09-10 |
* | Display number of available goals in "incorrect number of goals" error message. | Arnaud Spiwack | 2014-09-08 |
* | Add a tactic [revgoals] to reverse the list of focused goals. | Arnaud Spiwack | 2014-09-08 |
* | Renaming goal-entering functions. | Pierre-Marie Pédrot | 2014-09-06 |
* | Removing the old implementation of clear_body. | Pierre-Marie Pédrot | 2014-09-05 |
* | At last a working clearbody! | Pierre-Marie Pédrot | 2014-09-05 |
* | Only using filtered hyps in Goal.enter. | Pierre-Marie Pédrot | 2014-09-04 |
* | Ensuring the invariant that hypotheses and named context of the environment of | Pierre-Marie Pédrot | 2014-09-04 |
* | Revert the two previous commits. I was testing in the wrong branch. | Pierre-Marie Pédrot | 2014-09-04 |
* | Removing the old implementation of clear_body. | Pierre-Marie Pédrot | 2014-09-04 |
* | Fix: shelve_unifiable did not work modulo evar instantiation. | Arnaud Spiwack | 2014-09-04 |
* | Proofview refiner is now type-safe by default. | Pierre-Marie Pédrot | 2014-09-04 |
* | Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT. | Pierre-Marie Pédrot | 2014-09-04 |
* | Using goal-tactics to interpret arguments to idtac. | Pierre-Marie Pédrot | 2014-09-04 |
* | Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]." | Pierre-Marie Pédrot | 2014-09-04 |
* | Putting back normalized goals when entering them. | Pierre-Marie Pédrot | 2014-09-03 |
* | Simplify even further the declaration of primitive projections, | Matthieu Sozeau | 2014-08-30 |
* | Simplification of the tclCHECKINTERRUPT tactic. | Pierre-Marie Pédrot | 2014-08-28 |
* | Change the way primitive projections are declared to the kernel. | Matthieu Sozeau | 2014-08-28 |
* | Cleaning and documenting a bit the Proofview.Refine module. | Pierre-Marie Pédrot | 2014-08-28 |
* | "allows to", like "allowing to", is improper | Jason Gross | 2014-08-25 |
* | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau | 2014-08-22 |
* | Removing unused parts of the Goal.sensitive monad. | Pierre-Marie Pédrot | 2014-08-21 |
* | Removing a use of Goal.refine. | Pierre-Marie Pédrot | 2014-08-19 |
* | New primitive allowing to modify refine handles. | Pierre-Marie Pédrot | 2014-08-19 |
* | Improving error message when applying rewrite to an expression which is not a... | Hugo Herbelin | 2014-08-18 |
* | Reorganization of tactics: | Hugo Herbelin | 2014-08-18 |
* | More self-contained code for tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-15 |
* | Removing unused Refiner.tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-15 |
* | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot | 2014-08-07 |
* | Hypotheses in [Proofview.Goal.enter] were not normalised. | Arnaud Spiwack | 2014-08-07 |
* | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack | 2014-08-06 |
* | Adding a [make] primitive to the NonLogical monad. | Pierre-Marie Pédrot | 2014-08-05 |
* | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin | 2014-08-05 |
* | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin | 2014-08-05 |
* | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi | 2014-08-05 |
* | Goal: API to get the solution of a goal | Enrico Tassi | 2014-08-05 |
* | Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]. | Arnaud Spiwack | 2014-08-05 |
* | Some comments in the interface of Proofview_monad. | Arnaud Spiwack | 2014-08-04 |
* | Cleaning the new implementation of the tactic monad continued. | Arnaud Spiwack | 2014-08-04 |
* | Cleaning of the new implementation of the tactic monad. | Arnaud Spiwack | 2014-08-04 |
* | Add primtive [num_goal] to Proofview. | Arnaud Spiwack | 2014-08-01 |
* | Clean outdated comment in Proofview.Notations. | Arnaud Spiwack | 2014-08-01 |