| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès |
| 2017-04-03 | Merge branch 'v8.6' into trunk | Maxime Dénès |
| 2017-04-03 | Instances should obey universe binders even when defined by tactics. | Gaetan Gilbert |
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès |
| 2017-03-30 | Merge branch 'v8.6' into trunk | Maxime Dénès |
| 2017-03-29 | Run non-tactic comands without resilient_command | Tej Chajed |
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès |
| 2017-03-24 | Applying same convention as in Definition for printing type in a let in. | Hugo Herbelin |
| 2017-03-23 | A test checking for non-collision of name in irrefutable patterns. | Hugo Herbelin |
| 2017-03-21 | [pp] Make feedback the only logging mechanism. | Emilio Jesus Gallego Arias |
| 2017-03-14 | Report missing tactic arguments in error message | Tej Chajed |
| 2017-02-14 | Merge branch 'master'. | Pierre-Marie Pédrot |
| 2017-02-14 | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot |
