| Age | Commit message (Expand) | Author |
|---|
| 2016-06-27 | minor: comment on the meaning of the 'boolean' variable | Gabriel Scherer |
| 2016-06-27 | minor: documentation comment for constrintern.ml:sort_fields | Gabriel Scherer |
| 2016-06-27 | minor: interp/constrintern.ml, clarify field completion | Gabriel Scherer |
| 2016-06-27 | minor: in constrintern.ml:sort_fields, clarify sf | Gabriel Scherer |
| 2016-06-27 | minor: in constrintern.ml:sort_fields, clarify build_patt | Gabriel Scherer |
| 2016-06-27 | whitespace: untabity constrinternl.ml:sort_fields | Gabriel Scherer |
| 2016-06-27 | minor clarifications in constrintern.ml:sort_fields | Gabriel Scherer |
| 2016-06-27 | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre |
| 2016-06-16 | Not taking arguments given by name or position into account when | Hugo Herbelin |
| 2016-06-02 | A slight phase of documentation and uniformization of names of | Hugo Herbelin |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 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 |
