aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* 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
* | Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* | Fixing test-suite for bug #3043.Gravatar Pierre-Marie Pédrot2014-05-08
* | Fixing output test-suite: since universe polymorphism, the Print commandGravatar Pierre-Marie Pédrot2014-05-08
* | Code cleaning in Tacinterp: factorizing some uses of tclEVARS.Gravatar Pierre-Marie Pédrot2014-05-08
* | Removing comment outdated since eta holds in conversion rule (thisGravatar Hugo Herbelin2014-05-07
* | Adding test-suite for bug #3242.Gravatar Pierre-Marie Pédrot2014-05-06
| * Add regression tests for univ. poly. and prim projGravatar Jason Gross2014-05-06
|/
* Remove Lemmas from base_include, it's not linked in dev/printers anymoreGravatar Matthieu Sozeau2014-05-06
* Cleanup before merge with the trunkGravatar Matthieu Sozeau2014-05-06
* Use new tactic combinators in tclABSTRACT, to avoid blowup when using V82.tac...Gravatar Matthieu Sozeau2014-05-06
* Add missing case for primitive projection in fold_map.Gravatar Matthieu Sozeau2014-05-06
* Fix after merge.Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 11:48:41 +0000