| Age | Commit message (Expand) | Author |
|---|
| 2017-11-24 | When declaring constants/inductives use ContextSet if monomorphic. | Gaëtan Gilbert |
| 2017-11-24 | Fix defining non primitive projections with abstracted universes. | Gaëtan Gilbert |
| 2017-11-24 | Printing again "intros **" as "intros" by default. | Hugo Herbelin |
| 2017-11-24 | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). | Hugo Herbelin |
| 2017-11-22 | allow whitespace around infix op | Paul Steckler |
| 2017-11-22 | use OCaml criteria for infix ops, #6212 | Paul Steckler |
| 2017-11-20 | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic). | Hugo Herbelin |
| 2017-11-02 | Binding ltac printing functions to the system of generic printing. | Hugo Herbelin |
| 2017-10-19 | Moving bug numbers to BZ# format in the test-suite. | Théo Zimmermann |
| 2017-10-10 | 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-09 | Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on... | Maxime Dénès |
| 2017-10-04 | 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-09-25 | BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations | Paul Steckler |
| 2017-09-21 | Report missing arguments in error message | Tej Chajed |
| 2017-09-19 | 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-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 |
