| Commit message (Expand) | Author | Age |
* | Merge PR #834: Adding support for recursive notations of the form "x , .. , y... | Maxime Dénès | 2017-08-01 |
|\ |
|
* | | 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-26 |
|/ |
|
* | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | 2017-07-20 |
|\ |
|
| * | format pairs of items for pr_depth to get alternating separators | Paul Steckler | 2017-07-12 |
* | | Deprecate options that were introduced for compatibility with 8.5. | Théo Zimmermann | 2017-07-11 |
|/ |
|
* | 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-07 |
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-07-04 |
|\ \
| |/
|/| |
|
| * | Add tests for handling of warnings | Tej Chajed | 2017-06-23 |
* | | 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-14 |
* | | | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey | 2017-06-13 |
| | * | 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-09 |
|/ / |
|
* | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-06-08 |
|\| |
|
* | | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel. | Maxime Dénès | 2017-06-02 |
|\ \ |
|
| * | | [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-06-01 |
|\ \ \
| |/ /
|/| | |
|
| * | | Fixing a too lax constraint for finding recursive binder part of a notation. | Hugo Herbelin | 2017-05-31 |
* | | | Support for using type information to infer more precise evar sources. | Hugo Herbelin | 2017-05-30 |
|/ / |
|
| * | Merge PR#546: Fix for bug #4499 and other minor related bugs | Maxime Dénès | 2017-05-29 |
| |\ |
|
| * \ | Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show Match | Maxime Dénès | 2017-05-28 |
| |\ \ |
|
| * \ \ | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin... | Maxime Dénès | 2017-05-26 |
| |\ \ \ |
|
* | | | | | add Show test with -emacs flag | Paul Steckler | 2017-05-25 |
| | | * | | Bug 5546, qualify datatype constructors when needed | Paul Steckler | 2017-05-25 |
| | |/ /
| |/| | |
|
* | | | | 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-23 |
|\ \ \ \ \ |
|
| | * | | | | 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-20 |
| | * | | | add test for Show with -emacs, bug 5535 | Paul Steckler | 2017-05-19 |
* | | | | | 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-17 |
|\ \ \ \
| | |/ /
| |/| | |
|
| | * | | Simplified compaction criterion + tests. | Pierre Courtieu | 2017-05-16 |
| |/ /
|/| | |
|
| * | | remove unneeded -emacs flag to coq-prog-args | Paul Steckler | 2017-05-01 |
* | | | Remove VernacError | Gaetan Gilbert | 2017-04-21 |
* | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r... | Maxime Dénès | 2017-04-12 |
|\ \ \ |
|
| | | * | 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-07 |
|\ \ \ |
|
| * | | | [toplevel] Remove exception error printer in favor of feedback printer. | Emilio Jesus Gallego Arias | 2017-04-05 |
* | | | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-04-04 |
|\| | | |
|
| * | | | 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-04-03 |
| |\ \ \ |
|
| * \ \ \ | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-30 |
| |\ \ \ \
| | | |/ /
| | |/| | |
|
| | * | | | Run non-tactic comands without resilient_command | Tej Chajed | 2017-03-29 |
* | | | | | Merge branch 'trunk' into pr379 | Maxime Dénès | 2017-03-24 |
|\| | | | |
|