| Age | Commit message (Expand) | Author |
|---|
| 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-13 | 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-12 | 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-10 | Fix bug introduced by earlier commit on first-order unification of primitive | Matthieu Sozeau |
| 2014-08-09 | 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-08 | 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-07 | 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-06 | 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-05 | 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 | Preliminary re-installation of notation interpretation in beautifying mode. | Hugo Herbelin |
| 2014-08-05 | Testing beautifying on an example. | Hugo Herbelin |
| 2014-08-05 | Fixing a few beautifying bugs. | Hugo Herbelin |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | Testing a replacement of "cut" by "enough" on a couple of test files. | Hugo Herbelin |
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin |
| 2014-08-05 | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin |
| 2014-08-05 | More proofs independent of the names generated by induction/elim over | Hugo Herbelin |
| 2014-08-05 | Making references to Proof General and CoqIDE uniform in Reference Manual. | Hugo Herbelin |
