| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-06-25 | Putting implicit arguments of Clenv.res_pf right. | Pierre-Marie Pédrot |
| 2014-06-24 | 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-23 | Clenvtac.unify is in the new monad. | Pierre-Marie Pédrot |
| 2014-06-19 | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-06-17 | Tentative optimization not to nf_evar too often in the compatibility | Pierre-Marie Pédrot |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-17 | Safer entry point of primitive projections in the kernel, now it does recognize | Matthieu Sozeau |
| 2014-06-13 | Improving tclWITHHOLES which did not see undefined evars up to | Hugo Herbelin |
| 2014-06-13 | Fixing "clear" in internal_cut_replace: forbid dependencies in the | Hugo Herbelin |
| 2014-06-10 | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau |
| 2014-06-07 | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot |
