| Commit message (Expand) | Author | Age |
* | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). | Hugo Herbelin | 2017-11-20 |
* | Binding ltac printing functions to the system of generic printing. | Hugo Herbelin | 2017-11-02 |
* | Moving bug numbers to BZ# format in the test-suite. | Théo Zimmermann | 2017-10-19 |
* | Use a nice printer for constant names in Suggest Proof Using. | Gaëtan Gilbert | 2017-10-10 |
* | Take Suggest Proof Using outside the kernel. | Gaëtan Gilbert | 2017-10-10 |
* | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on... | Maxime Dénès | 2017-10-09 |
|\ |
|
* \ | Merge PR #1078: Report missing arguments in error message | Maxime Dénès | 2017-10-04 |
|\ \ |
|
* \ \ | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial). | Maxime Dénès | 2017-10-04 |
|\ \ \ |
|
| | | * | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler | 2017-09-25 |
| | * | | Report missing arguments in error message | Tej Chajed | 2017-09-21 |
| | |/ |
|
| * / | Fixing bug #5741 (anomaly in info_trivial). | Hugo Herbelin | 2017-09-19 |
| |/ |
|
* / | Don't lose names in UState.universe_context. | Gaëtan Gilbert | 2017-09-19 |
|/ |
|
* | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work... | Maxime Dénès | 2017-09-15 |
|\ |
|
* | | 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-09-12 |
* | | 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-29 |
| * | Ensuring all .v files end with a newline to make "sed -i" work better on them. | Hugo Herbelin | 2017-08-21 |
|/ |
|
* | Print names of all open blocks | Tej Chajed | 2017-08-06 |
* | 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 |