| Commit message (Expand) | Author | Age |
|---|
| * | "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 |
| * | Removing more tactic compatibility layer. | Pierre-Marie Pédrot | 2014-08-01 |
| * | Making the error message about bullets more precise. |  Pierre Courtieu | 2014-07-31 |
| * | Adding a tclBREAK primitive to the tactic monad. | Pierre-Marie Pédrot | 2014-07-28 |
| * | 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-25 |
| * | 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-24 |
| * | 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-23 |
| * | Adding a delay to tclTIME. | Pierre-Marie Pédrot | 2014-07-14 |
| * | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin | 2014-07-13 |
| * | Feedback: LoadedFile + Goals | Enrico Tassi | 2014-07-11 |
| * | check_for_interrupt: better (but slower) in threading mode | Enrico Tassi | 2014-07-10 |
| * | Exporting Proof.split in proofview. | Pierre-Marie Pédrot | 2014-07-08 |
| * | Revert "time tac" (committed by mistake). | Hugo Herbelin | 2014-07-07 |
| * | time tac | Hugo Herbelin | 2014-07-07 |
| * | Putting implicit arguments of Clenv.res_pf right. | Pierre-Marie Pédrot | 2014-06-25 |
| * | Force the final universe context of a proof only in poly || now case. | Matthieu Sozeau | 2014-06-24 |
| * | Clenvtac.clenv_refine in the new monad. Not satisfactory though, because it | Pierre-Marie Pédrot | 2014-06-24 |
| * | Clenvtac.res_pf is in the new tactic monad. | Pierre-Marie Pédrot | 2014-06-24 |
| * | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot | 2014-06-23 |
Jason Gross
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Arnaud Spiwack
Enrico Tassi
Pierre Courtieu