| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Moving the TacAlias node out of atomic tactics. |  Pierre-Marie Pédrot | 2014-08-18 |
| * | Moving the TacExtend node from atomic to plain tactics. | Pierre-Marie Pédrot | 2014-08-18 |
| * | Removing documentation related to the deprecated State machinery. | Pierre-Marie Pédrot | 2014-08-16 |
| * | Better printing of Ltac values. | Pierre-Marie Pédrot | 2014-08-16 |
| * | Fixing too restrictive detection of resolution of evars in "apply in" |  Hugo Herbelin | 2014-08-16 |
| * | More self-contained code for tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-15 |
| * | Removing unused Refiner.tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-15 |
| * | Remove confusing behavior of unify_with_subterm that could fail with |  Matthieu Sozeau | 2014-08-14 |
| * | Fix program using an the unsubstituted type of the original obligation | Matthieu Sozeau | 2014-08-14 |
| * | Fix non-printing of coercions for primitive projections (fixes bug #3433). | Matthieu Sozeau | 2014-08-14 |
| * | Restrict eta-conversion to inductive records, fixing bug #3310. | Matthieu Sozeau | 2014-08-14 |
| * | Restore the error-handling behavior of [change], which was silently failing | Matthieu Sozeau | 2014-08-14 |
| * | Fix elimschemes accessing directly the universe context of inductives (fixes ... | Matthieu Sozeau | 2014-08-14 |
| * | Fix test-suite files according to new parsing rule for application of primitive | Matthieu Sozeau | 2014-08-13 |
| * | Small optimization in Cooking: do not construct identity substitutions. | Pierre-Marie Pédrot | 2014-08-13 |
| * | Bettre pretty-printing of evar maps, avoids printing universe information | Matthieu Sozeau | 2014-08-13 |
| * | Upgrading output tests. | Hugo Herbelin | 2014-08-12 |
| * | Bug #3469: fixing unterminated comment. | Hugo Herbelin | 2014-08-12 |
| * | In bug #2406, renouncing to test failure of parsing error. | Hugo Herbelin | 2014-08-12 |
| * | Quick fix for avoiding infinitely many respawning and Warning "Coq | Hugo Herbelin | 2014-08-12 |
| * | Fixing parsing of bullets after a "...". | Hugo Herbelin | 2014-08-12 |
| * | A couple of fixes/improvements in -beautify, but backtracking on | Hugo Herbelin | 2014-08-12 |
| * | Fix bug introduced by earlier commit on first-order unification of primitive |  Matthieu Sozeau | 2014-08-10 |
| * | Fix unification which was failing when unifying a primitive projection against | Matthieu Sozeau | 2014-08-09 |
| * | Allow pattern matching on the applied form of projections with primitive | Matthieu Sozeau | 2014-08-09 |
| * | Do early occur-check in unification to allow eta to fire (fixes bug #3477) | Matthieu Sozeau | 2014-08-09 |
| * | Using the asymmetric merging primitive in Evd. | Pierre-Marie Pédrot | 2014-08-09 |
| * | Adding a primitive to merge ContextSets which is more efficient when one | Pierre-Marie Pédrot | 2014-08-09 |
| * | Cleaning up interface of ContextSet. | Pierre-Marie Pédrot | 2014-08-09 |
| * | Tentative performance fix for Evd.merge_uctx. | Pierre-Marie Pédrot | 2014-08-09 |
| * | Change internalization of primitive projections to allow parsing [p t] as | Matthieu Sozeau | 2014-08-08 |
| * | Fix evarconv not applying eta when it used to. Fixes bug#3319. | Matthieu Sozeau | 2014-08-08 |
| * | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot | 2014-08-07 |
| * | More .mailmap update. |  Arnaud Spiwack | 2014-08-07 |
| * | Add some more entries to .mailmap | Arnaud Spiwack | 2014-08-07 |
| * | Hypotheses in [Proofview.Goal.enter] were not normalised. | Arnaud Spiwack | 2014-08-07 |
| * | In Hipattern: some functions not working modulo evar instantiation. | Arnaud Spiwack | 2014-08-07 |
| * | Removing simple induction / destruct from the AST. | Pierre-Marie Pédrot | 2014-08-07 |
| * | Instead of relying on a trick to make the constructor tactic parse, put | Pierre-Marie Pédrot | 2014-08-07 |
| * | Removing the "constructor" tactic from the AST. | Pierre-Marie Pédrot | 2014-08-07 |
| * | Port last changes of the guard condition to checker. |  Maxime Dénès | 2014-08-06 |
| * | Relax a bit the guard condition. | Maxime Dénès | 2014-08-06 |
| * | Revert the change in Constrintern introduced by "Add a type of untyped term t... | Arnaud Spiwack | 2014-08-06 |
| * | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack | 2014-08-06 |
| * | Removing "intros untils" from the AST. | Pierre-Marie Pédrot | 2014-08-06 |
| * | Adding a [make] primitive to the NonLogical monad. | Pierre-Marie Pédrot | 2014-08-05 |
| * | Small code simplification. | Pierre-Marie Pédrot | 2014-08-05 |
| * | CoqIDE: fixing parsing of bullets and brackets even at end of file. | Hugo Herbelin | 2014-08-05 |
| * | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin | 2014-08-05 |
| * | Improving printing of "[]" (nil) in spite of the risk of collision | Hugo Herbelin | 2014-08-05 |
Pierre-Marie Pédrot
Hugo Herbelin
Matthieu Sozeau
Matthieu Sozeau
Arnaud Spiwack
Maxime Dénès