aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* | Simplification and improvement of "subst x" in such a way that itGravatar Hugo Herbelin2014-05-08
* | Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
* | Little reorganization of generalize tactics code w/o semantic changes.Gravatar Hugo Herbelin2014-05-08
* | Cleanup code in pretyping/evarutilGravatar Matthieu Sozeau2014-05-08
* | Fix performance problem with unification in presence of universes (bug #3302)...Gravatar Matthieu Sozeau2014-05-08
* | - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Gravatar Matthieu Sozeau2014-05-08
* | Avoid allocations in type_of_inductiveGravatar Matthieu Sozeau2014-05-08
* | Fast-path equality of sorts in compare_constr*Gravatar Matthieu Sozeau2014-05-08
* | Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-04 09:10:21 +0000