| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Adding a raw_goals primitive for Tacinterp. | Pierre-Marie Pédrot | 2014-06-19 |
| * | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
| * | 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-17 |
| * | 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-13 |
| * | Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un... | Matthieu Sozeau | 2014-06-10 |
| * | Adding a new Control file centralizing the control options of Coq. | Pierre-Marie Pédrot | 2014-06-07 |
Pierre-Marie Pédrot
Arnaud Spiwack
Hugo Herbelin
Enrico Tassi
Pierre Courtieu
Matthieu Sozeau