| Age | Commit message (Expand) | Author |
|---|
| 2016-03-13 | Adopting the same rules for interpreting @, abbreviations and | Hugo Herbelin |
| 2016-03-13 | Supporting "(@foo) args" in patterns, where "@foo" has no arguments. | Hugo Herbelin |
| 2016-03-12 | A more explicit name to the asymmetric boolean flag. | Hugo Herbelin |
| 2016-02-28 | Printing notations: Cleaning in anticipation of fixing #4592. | Hugo Herbelin |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2016-01-11 | CLEANUP: removing unused field | Matej Kosik |
| 2016-01-11 | merge | Matej Kosik |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2016-01-02 | Remove some unused functions. | Guillaume Melquiond |
| 2015-12-31 | Do not compose List.length with List.filter. | Guillaume Melquiond |
| 2015-12-18 | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified | Matej Kosik |
| 2015-11-11 | Fixing bug #3554: Anomaly: Anonymous implicit argument. | Pierre-Marie Pédrot |
| 2015-09-16 | Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #... | Guillaume Melquiond |
| 2015-08-21 | Fixing #4318 (anomaly when applying args to a recursive notation in patterns). | Hugo Herbelin |
| 2015-07-27 | Fixing #4305 (compatibility wrt 8.4 in not interpreting an | Hugo Herbelin |
| 2015-05-01 | Fixing computation of implicit arguments by position in fixpoints (#4217). | Hugo Herbelin |
| 2015-04-21 | Fixing #3376 and #4191 (wrong index of maximally-inserted implicit argument | Hugo Herbelin |
| 2015-02-27 | Removing the unused field ltacrecvars of tactic internalization. | Pierre-Marie Pédrot |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-30 | Fixing #3892: Ensure that notation variables do not capture names | Hugo Herbelin |
| 2014-12-11 | Tentatively more informative report of failure when inferring | Hugo Herbelin |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-27 | Add a boolean to indicate the unfolding state of a primitive projection, | Matthieu Sozeau |
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-09-12 | Parsing evar instances. | Hugo Herbelin |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-10 | Parsing and printing of primitive projections, fix buggy behavior when | Matthieu Sozeau |
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau |
| 2014-09-08 | Parsing of Type@{max(i,j)}. | Matthieu Sozeau |
| 2014-08-08 | Change internalization of primitive projections to allow parsing [p t] as | Matthieu Sozeau |
| 2014-08-06 | Revert the change in Constrintern introduced by "Add a type of untyped term t... | Arnaud Spiwack |
| 2014-08-05 | Better fix of e5c025 | Pierre Boutillier |
| 2014-08-03 | Fixing #3483 (graceful failing with notations to non-constructors in "match"). | Hugo Herbelin |
| 2014-08-02 | Better struture for Ltac internalization environments in Constrintern. | Pierre-Marie Pédrot |
| 2014-08-01 | Faster uconstr. | Arnaud Spiwack |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-07-31 | Finish fixes on notations and primitive projections, add test-suite files for... | Matthieu Sozeau |
| 2014-07-29 | Add a type of untyped term to Ltac's value. | Arnaud Spiwack |
| 2014-07-29 | Fix treatment of notations containing applications of projections (fixes bug ... | Matthieu Sozeau |
| 2014-06-17 | Continue fix on argument scopes of primitive projections. | Matthieu Sozeau |
| 2014-06-17 | Fixing #3282 (two bugs in the presence of let-in's in "fix"). | Hugo Herbelin |
| 2014-06-17 | Removing dead code. | Pierre-Marie Pédrot |
| 2014-06-11 | Fix bug #3289 | Matthieu Sozeau |
| 2014-06-04 | Collecting in Namegen those conventional default names that are used in diffe... | Hugo Herbelin |
| 2014-06-04 | - Fix hashing of levels to get the "right" order in universe contexts etc... | Matthieu Sozeau |
| 2014-05-06 | Fix printing of projections with implicits. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
