| Age | Commit message (Expand) | Author |
|---|
| 2017-09-15 | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work... | Maxime Dénès |
| 2017-09-12 | Fixing bug #5693 (treating empty notation format as any format). | Hugo Herbelin |
| 2017-09-12 | Fixing a bug of recursive notations introduced in dfdaf4de. | Hugo Herbelin |
| 2017-08-29 | Adding a test for #5569 (warning about skipping spaces). | Hugo Herbelin |
| 2017-08-29 | A little reorganization of notations + a fix to #5608. | Hugo Herbelin |
| 2017-08-21 | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin |
| 2017-08-06 | Print names of all open blocks | Tej Chajed |
| 2017-08-01 | Merge PR #834: Adding support for recursive notations of the form "x , .. , y... | Maxime Dénès |
| 2017-07-26 | Fix TypeclassDebug.out after conflicting PR merges | Matthieu Sozeau |
| 2017-07-26 | Adding support for recursive notations of the form "x , .. , y , z". | Hugo Herbelin |
| 2017-07-20 | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès |
| 2017-07-12 | format pairs of items for pr_depth to get alternating separators | Paul Steckler |
| 2017-07-11 | Deprecate options that were introduced for compatibility with 8.5. | Théo Zimmermann |
| 2017-07-07 | Merge PR #863: Fixing environment in warning "Projection value has no head co... | Maxime Dénès |
| 2017-07-07 | Fixing environment in warning "Projection value has no head constant". | Hugo Herbelin |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-06-23 | Add tests for handling of warnings | Tej Chajed |
| 2017-06-14 | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match"). | Maxime Dénès |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey |
| 2017-06-09 | Fix Bug #5568, no dup notation warnings on repeated module imports | Paul Steckler |
| 2017-06-09 | A fix to #5414 (ident bound by ltac names now known for "match"). | Hugo Herbelin |
| 2017-06-08 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-06-02 | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel. | Maxime Dénès |
| 2017-06-01 | [emacs] [toplevel] Make emacs flag local to the toplevel. | Emilio Jesus Gallego Arias |
| 2017-06-01 | Merge PR#694: Fixing #5523 (missing support for complex constructions in recu... | Maxime Dénès |
| 2017-05-31 | Fixing a too lax constraint for finding recursive binder part of a notation. | Hugo Herbelin |
| 2017-05-30 | Support for using type information to infer more precise evar sources. | Hugo Herbelin |
| 2017-05-29 | Merge PR#546: Fix for bug #4499 and other minor related bugs | Maxime Dénès |
| 2017-05-28 | Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show Match | Maxime Dénès |
| 2017-05-26 | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin... | Maxime Dénès |
| 2017-05-25 | add Show test with -emacs flag | Paul Steckler |
| 2017-05-25 | Bug 5546, qualify datatype constructors when needed | Paul Steckler |
| 2017-05-23 | Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit... | Maxime Dénès |
| 2017-05-23 | Merge PR#657: [test-suite] Add tests for goal printing. | Maxime Dénès |
| 2017-05-20 | Added a test for #4765 (an example of printing abbreviation with binders). | Hugo Herbelin |
| 2017-05-20 | [test-suite] Add tests for goal printing. | Emilio Jesus Gallego Arias |
| 2017-05-19 | add test for Show with -emacs, bug 5535 | Paul Steckler |
| 2017-05-17 | A fix for #5390 (a useful error on used introduction names was masked). | Hugo Herbelin |
| 2017-05-17 | Fixing bug #5526,allow nonlinear variables in Notation patterns | Paul Steckler |
| 2017-05-17 | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès |
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-05-16 | Simplified compaction criterion + tests. | Pierre Courtieu |
| 2017-05-01 | remove unneeded -emacs flag to coq-prog-args | Paul Steckler |
| 2017-04-21 | Remove VernacError | Gaetan Gilbert |
| 2017-04-12 | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r... | Maxime Dénès |
| 2017-04-07 | Better support for printing constructors with let-ins. | Hugo Herbelin |
| 2017-04-07 | Fixing #4499 (not using unnamed record field in {| |} notation). | Hugo Herbelin |
| 2017-04-07 | Merge branch 'master' into econstr | Pierre-Marie Pédrot |
| 2017-04-05 | [toplevel] Remove exception error printer in favor of feedback printer. | Emilio Jesus Gallego Arias |
