| Age | Commit message (Expand) | Author |
|---|
| 2014-09-08 | Add a tactic [revgoals] to reverse the list of focused goals. | Arnaud Spiwack |
| 2014-09-06 | Renaming goal-entering functions. | Pierre-Marie Pédrot |
| 2014-09-05 | 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-04 | 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-03 | Putting back normalized goals when entering them. | Pierre-Marie Pédrot |
| 2014-08-30 | Simplify even further the declaration of primitive projections, | Matthieu Sozeau |
| 2014-08-28 | 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-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-22 | Move UnsatisfiableConstraints to a pretype error. | Matthieu Sozeau |
| 2014-08-21 | Removing unused parts of the Goal.sensitive monad. | Pierre-Marie Pédrot |
| 2014-08-19 | 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-18 | 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-15 | More self-contained code for tclWITHHOLES. | Pierre-Marie Pédrot |
| 2014-08-15 | Removing unused Refiner.tclWITHHOLES. | Pierre-Marie Pédrot |
| 2014-08-07 | 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-06 | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack |
| 2014-08-05 | 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-04 | 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-01 | Add primtive [num_goal] to Proofview. | Arnaud Spiwack |
| 2014-08-01 | Clean outdated comment in Proofview.Notations. | Arnaud Spiwack |
| 2014-08-01 | Removing more tactic compatibility layer. | Pierre-Marie Pédrot |
| 2014-07-31 | Making the error message about bullets more precise. | Pierre Courtieu |
| 2014-07-28 | Adding a tclBREAK primitive to the tactic monad. | Pierre-Marie Pédrot |
| 2014-07-25 | Add a tactic [swap i j] to swap the position of goals [i] and [j]. | Arnaud Spiwack |
| 2014-07-25 | Adds a cycle tactic to reorder goals in a loop. | Arnaud Spiwack |
| 2014-07-25 | Small reorganisation in proof.ml. | Arnaud Spiwack |
| 2014-07-25 | Fail gracefully when focusing on non-existing goals with user commands. | Arnaud Spiwack |
| 2014-07-25 | Fix handling of universes at the end of proofs, esp. for async proof processing. | Matthieu Sozeau |
| 2014-07-24 | A handful of useful primitives in Proofview.Refine. | Arnaud Spiwack |
