aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* Tactics declared through TACTIC EXTEND that are of the formGravatar Pierre-Marie Pédrot2014-05-20
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-05-20
* Revert "Fix Qcanon after changes on injection."Gravatar Maxime Dénès2014-05-18
* When discrimination is not possible, try to project.Gravatar Maxime Dénès2014-05-18
* Suggest Set Injection On Proofs in error message for injection.Gravatar Maxime Dénès2014-05-18
* Restored old behavior of injection on proofs by default.Gravatar Maxime Dénès2014-05-18
* Adding way to get the list of the accepted tactic notation arguments.Gravatar Pierre-Marie Pédrot2014-05-17
* Fixing coqdep_boot warning relative to unknown ML files that were in tactics.Gravatar Pierre-Marie Pédrot2014-05-17
* Fixing Camlp4 compilationGravatar Pierre-Marie Pédrot2014-05-17
* Revert "Decent error message when a constant is not found"Gravatar Enrico Tassi2014-05-16
* More fixes of unification with primitive projections (missed cases during the...Gravatar Matthieu Sozeau2014-05-16
* Declare: fix Future managementGravatar Enrico Tassi2014-05-16
* Decent error message when a constant is not foundGravatar Enrico Tassi2014-05-16
* Fix unification of non-unfoldable primitive projections in evarconv.Gravatar Matthieu Sozeau2014-05-16
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* Slightly better printer for native ML tactics, in order to disambiguateGravatar Pierre-Marie Pédrot2014-05-16
* Tactics defined through TACTIC EXTEND that are only defined as a string doGravatar Pierre-Marie Pédrot2014-05-16
* Another try at close_proof that should behave better w.r.t. exception handling.Gravatar Matthieu Sozeau2014-05-16
* heads: avoid forcing opaque proofsGravatar Enrico Tassi2014-05-15
* poly: remove unused attribute to STM nodes and vernac classificaitonGravatar Enrico Tassi2014-05-15
* Polymorphic Lemmas are like Defined ones for STMGravatar Enrico Tassi2014-05-15
* Future: better error messageGravatar Enrico Tassi2014-05-15
* Fix the behaviour of ML tactic notations w.r.t. Imports by making themGravatar Pierre-Marie Pédrot2014-05-13
* Test-suite for bug #3259.Gravatar Pierre-Marie Pédrot2014-05-13
* Rewritten the sorting algorithm for universes with a better complexity.Gravatar Pierre-Marie Pédrot2014-05-13
* Update various polyproj bugs w.r.t. latest trunkGravatar Jason Gross2014-05-12
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Moving the ML tactic extension mechanism to a Libobject-based one.Gravatar Pierre-Marie Pédrot2014-05-12
* Plugin names must be declared in the header of .ml4 file, be they static orGravatar Pierre-Marie Pédrot2014-05-12
* Adding the possibility for ML modules to declare functions to be called atGravatar Pierre-Marie Pédrot2014-05-12
* Fixing the undocumented -dumpgraphbox option of coqdep.Gravatar Pierre-Marie Pédrot2014-05-12
* Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,Gravatar Pierre-Marie Pédrot2014-05-11
* Eliminating a potentially quadratic behaviour in Require, by using mapsGravatar Pierre-Marie Pédrot2014-05-11
* Add appropriate Fail(s) to opened bugsGravatar Jason Gross2014-05-10
* Move opened bugs to bugs/openedGravatar Jason Gross2014-05-10
* Add more regression tests for univ poly/prim projGravatar Jason Gross2014-05-10
* Code cleaning & factorizing functions in Equality.Gravatar Pierre-Marie Pédrot2014-05-09
* Update and start testing rewrite-in-type code.Gravatar Matthieu Sozeau2014-05-09
* More documentation of new features in CHANGE.Gravatar Pierre-Marie Pédrot2014-05-09
* Refresh universes for Ltac's type_of, as the term can be used anywhere,Gravatar Matthieu Sozeau2014-05-09
* Merge branch 'working-polyproj-tests' of https://github.com/JasonGross/coq in...Gravatar Matthieu Sozeau2014-05-09
|\
* | Fix second-order matching to properly check that the predicate found byGravatar Matthieu Sozeau2014-05-09
* | Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
* | Reuse universe level substitutions for template polymorphism, fixing performanceGravatar Matthieu Sozeau2014-05-09
* | Encapsulating some clausenv uses. This simplifies the control flow of someGravatar Pierre-Marie Pédrot2014-05-08
* | Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Gravatar Hugo Herbelin2014-05-08
* | Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Gravatar Hugo Herbelin2014-05-08
* | Typo reference manualGravatar Hugo Herbelin2014-05-08
* | Isolating a function "make_abstraction", new name of "letin_abstract",Gravatar Hugo Herbelin2014-05-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 18:06:05 +0000