aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-05-21Removing decompose record / sum from the tactic AST.Pierre-Marie Pédrot
2014-05-21Allowing Ltac definitions that may be unusable because of a built-inPierre-Marie Pédrot
2014-05-21Moving left & right tactics out of the AST.Pierre-Marie Pédrot
2014-05-20Moving (e)transitivity out of the AST.Pierre-Marie Pédrot
2014-05-20Tactics declared through TACTIC EXTEND that are of the formPierre-Marie Pédrot
2014-05-20Tentative to add constr-using primitive tactics without grammar rules.Pierre-Marie Pédrot
2014-05-18Revert "Fix Qcanon after changes on injection."Maxime Dénès
2014-05-18When discrimination is not possible, try to project.Maxime Dénès
2014-05-18Suggest Set Injection On Proofs in error message for injection.Maxime Dénès
2014-05-18Restored old behavior of injection on proofs by default.Maxime Dénès
2014-05-17Adding way to get the list of the accepted tactic notation arguments.Pierre-Marie Pédrot
2014-05-17Fixing coqdep_boot warning relative to unknown ML files that were in tactics.Pierre-Marie Pédrot
2014-05-17Fixing Camlp4 compilationPierre-Marie Pédrot
2014-05-16Revert "Decent error message when a constant is not found"Enrico Tassi
2014-05-16More fixes of unification with primitive projections (missed cases during the...Matthieu Sozeau
2014-05-16Declare: fix Future managementEnrico Tassi
2014-05-16Decent error message when a constant is not foundEnrico Tassi
2014-05-16Fix unification of non-unfoldable primitive projections in evarconv.Matthieu Sozeau
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
2014-05-16Slightly better printer for native ML tactics, in order to disambiguatePierre-Marie Pédrot
2014-05-16Tactics defined through TACTIC EXTEND that are only defined as a string doPierre-Marie Pédrot
2014-05-16Another try at close_proof that should behave better w.r.t. exception handling.Matthieu Sozeau
2014-05-15heads: avoid forcing opaque proofsEnrico Tassi
2014-05-15poly: remove unused attribute to STM nodes and vernac classificaitonEnrico Tassi
2014-05-15Polymorphic Lemmas are like Defined ones for STMEnrico Tassi
2014-05-15Future: better error messageEnrico Tassi
2014-05-13Fix the behaviour of ML tactic notations w.r.t. Imports by making themPierre-Marie Pédrot
2014-05-13Test-suite for bug #3259.Pierre-Marie Pédrot
2014-05-13Rewritten the sorting algorithm for universes with a better complexity.Pierre-Marie Pédrot
2014-05-12Update various polyproj bugs w.r.t. latest trunkJason Gross
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-12Moving the ML tactic extension mechanism to a Libobject-based one.Pierre-Marie Pédrot
2014-05-12Plugin names must be declared in the header of .ml4 file, be they static orPierre-Marie Pédrot
2014-05-12Adding the possibility for ML modules to declare functions to be called atPierre-Marie Pédrot
2014-05-12Fixing the undocumented -dumpgraphbox option of coqdep.Pierre-Marie Pédrot
2014-05-11Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,Pierre-Marie Pédrot
2014-05-11Eliminating a potentially quadratic behaviour in Require, by using mapsPierre-Marie Pédrot
2014-05-10Add appropriate Fail(s) to opened bugsJason Gross
2014-05-10Move opened bugs to bugs/openedJason Gross
2014-05-10Add more regression tests for univ poly/prim projJason Gross
2014-05-09Code cleaning & factorizing functions in Equality.Pierre-Marie Pédrot
2014-05-09Update and start testing rewrite-in-type code.Matthieu Sozeau
2014-05-09More documentation of new features in CHANGE.Pierre-Marie Pédrot
2014-05-09Refresh universes for Ltac's type_of, as the term can be used anywhere,Matthieu Sozeau
2014-05-09Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq in...Matthieu Sozeau
2014-05-09Fix second-order matching to properly check that the predicate found byMatthieu Sozeau
2014-05-09Restore implicit arguments of irreflexivity (fixes bug #3305).Matthieu Sozeau
2014-05-09Reuse universe level substitutions for template polymorphism, fixing performanceMatthieu Sozeau
2014-05-08Encapsulating some clausenv uses. This simplifies the control flow of somePierre-Marie Pédrot
2014-05-08Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 17:41:18 +0000