| Age | Commit message (Expand) | Author |
|---|
| 2014-05-20 | Tactics declared through TACTIC EXTEND that are of the form | Pierre-Marie Pédrot |
| 2014-05-20 | Tentative to add constr-using primitive tactics without grammar rules. | Pierre-Marie Pédrot |
| 2014-05-18 | Revert "Fix Qcanon after changes on injection." | Maxime Dénès |
| 2014-05-18 | When discrimination is not possible, try to project. | Maxime Dénès |
| 2014-05-18 | Suggest Set Injection On Proofs in error message for injection. | Maxime Dénès |
| 2014-05-18 | Restored old behavior of injection on proofs by default. | Maxime Dénès |
| 2014-05-17 | Adding way to get the list of the accepted tactic notation arguments. | Pierre-Marie Pédrot |
| 2014-05-17 | Fixing coqdep_boot warning relative to unknown ML files that were in tactics. | Pierre-Marie Pédrot |
| 2014-05-17 | Fixing Camlp4 compilation | Pierre-Marie Pédrot |
| 2014-05-16 | Revert "Decent error message when a constant is not found" | Enrico Tassi |
| 2014-05-16 | More fixes of unification with primitive projections (missed cases during the... | Matthieu Sozeau |
| 2014-05-16 | Declare: fix Future management | Enrico Tassi |
| 2014-05-16 | Decent error message when a constant is not found | Enrico Tassi |
| 2014-05-16 | Fix unification of non-unfoldable primitive projections in evarconv. | Matthieu Sozeau |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot |
| 2014-05-16 | Slightly better printer for native ML tactics, in order to disambiguate | Pierre-Marie Pédrot |
| 2014-05-16 | Tactics defined through TACTIC EXTEND that are only defined as a string do | Pierre-Marie Pédrot |
| 2014-05-16 | Another try at close_proof that should behave better w.r.t. exception handling. | Matthieu Sozeau |
| 2014-05-15 | heads: avoid forcing opaque proofs | Enrico Tassi |
| 2014-05-15 | poly: remove unused attribute to STM nodes and vernac classificaiton | Enrico Tassi |
| 2014-05-15 | Polymorphic Lemmas are like Defined ones for STM | Enrico Tassi |
| 2014-05-15 | Future: better error message | Enrico Tassi |
| 2014-05-13 | Fix the behaviour of ML tactic notations w.r.t. Imports by making them | Pierre-Marie Pédrot |
| 2014-05-13 | Test-suite for bug #3259. | Pierre-Marie Pédrot |
| 2014-05-13 | Rewritten the sorting algorithm for universes with a better complexity. | Pierre-Marie Pédrot |
| 2014-05-12 | Update various polyproj bugs w.r.t. latest trunk | Jason Gross |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-05-12 | Moving the ML tactic extension mechanism to a Libobject-based one. | Pierre-Marie Pédrot |
| 2014-05-12 | Plugin names must be declared in the header of .ml4 file, be they static or | Pierre-Marie Pédrot |
| 2014-05-12 | Adding the possibility for ML modules to declare functions to be called at | Pierre-Marie Pédrot |
| 2014-05-12 | Fixing the undocumented -dumpgraphbox option of coqdep. | Pierre-Marie Pédrot |
| 2014-05-11 | Using Maps to handle imports in Safe_typing. The order is irrelevant indeed, | Pierre-Marie Pédrot |
| 2014-05-11 | Eliminating a potentially quadratic behaviour in Require, by using maps | Pierre-Marie Pédrot |
| 2014-05-10 | Add appropriate Fail(s) to opened bugs | Jason Gross |
| 2014-05-10 | Move opened bugs to bugs/opened | Jason Gross |
| 2014-05-10 | Add more regression tests for univ poly/prim proj | Jason Gross |
| 2014-05-09 | Code cleaning & factorizing functions in Equality. | Pierre-Marie Pédrot |
| 2014-05-09 | Update and start testing rewrite-in-type code. | Matthieu Sozeau |
| 2014-05-09 | More documentation of new features in CHANGE. | Pierre-Marie Pédrot |
| 2014-05-09 | Refresh universes for Ltac's type_of, as the term can be used anywhere, | Matthieu Sozeau |
| 2014-05-09 | Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq in... | Matthieu Sozeau |
| 2014-05-09 | Fix second-order matching to properly check that the predicate found by | Matthieu Sozeau |
| 2014-05-09 | Restore implicit arguments of irreflexivity (fixes bug #3305). | Matthieu Sozeau |
| 2014-05-09 | Reuse universe level substitutions for template polymorphism, fixing performance | Matthieu Sozeau |
| 2014-05-08 | Encapsulating some clausenv uses. This simplifies the control flow of some | Pierre-Marie Pédrot |
| 2014-05-08 | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic." | Hugo Herbelin |
| 2014-05-08 | Avoid "revert" to retype-check the goal, and move it to a "new" tactic. | Hugo Herbelin |
| 2014-05-08 | Typo reference manual | Hugo Herbelin |
| 2014-05-08 | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin |
| 2014-05-08 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin |
