| Age | Commit message (Expand) | Author |
|---|
| 2016-05-04 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-05-03 | Fix bug #3825: Universe annotations on notations should pass through or be re... | Pierre-Marie Pédrot |
| 2016-04-27 | Revert "Not taking arguments given by name or position into account when" | Hugo Herbelin |
| 2016-04-27 | Revert "Warn about possible shadowing of a name occurring in a "in" clause." | Hugo Herbelin |
| 2016-04-27 | Warn about possible shadowing of a name occurring in a "in" clause. | Hugo Herbelin |
| 2016-04-27 | Not taking arguments given by name or position into account when | Hugo Herbelin |
| 2016-04-27 | Fixing a "This clause is redundant" error when interpreting the "in" | Hugo Herbelin |
| 2016-04-27 | Reformatting + removal of some useless data + some cut-elimination | Hugo Herbelin |
| 2016-04-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau |
| 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-08-14 | Move type_scope into user space, fix some output logs | Jason Gross |
| 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 |
