| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-07-24 | Adding a tail-rec tclONCE. | Pierre-Marie Pédrot |
| 2014-07-24 | New implementation of the tactic monad. | Pierre-Marie Pédrot |
| 2014-07-23 | When closing a proof, make sure that the types have their evar substituted. | Arnaud Spiwack |
| 2014-07-23 | Proof_global: an unused variable replaced by a wildcard. | Arnaud Spiwack |
| 2014-07-23 | Proof_global.start_dependent_proof: properly threads the sigma through the te... | Arnaud Spiwack |
| 2014-07-23 | Change the interface of proof_global to take an evar_map instead of a univers... | Arnaud Spiwack |
| 2014-07-14 | Adding a delay to tclTIME. | Pierre-Marie Pédrot |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin |
| 2014-07-11 | Feedback: LoadedFile + Goals | Enrico Tassi |
| 2014-07-10 | check_for_interrupt: better (but slower) in threading mode | Enrico Tassi |
| 2014-07-08 | Exporting Proof.split in proofview. | Pierre-Marie Pédrot |
| 2014-07-07 | Revert "time tac" (committed by mistake). | Hugo Herbelin |
| 2014-07-07 | time tac | Hugo Herbelin |
