aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output
Commit message (Expand)AuthorAge
* Merge remote-tracking branch 'github/pr/319' into v8.6Gravatar Maxime Dénès2016-10-28
|\
* \ Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
|\ \
| * | Add missing dot to impargs error message.Gravatar Maxime Dénès2016-10-27
| * | Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | | Adding a test for #4398 (interpretation scopes for "match goal").Gravatar Hugo Herbelin2016-10-24
* | | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-22
|\ \ \
| * | | Fixing printing of generic arguments of tag "var".Gravatar Hugo Herbelin2016-10-22
* | | | Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Gravatar Matthieu Sozeau2016-10-21
* | | | [search] Don't build intermediate lists in search.Gravatar Emilio Jesus Gallego Arias2016-10-20
* | | | Test for variant of #5142 (good error message on pattern-matching failure).Gravatar Hugo Herbelin2016-10-19
* | | | Attempt to improve error rendering in pattern-matching compilation (#5142).Gravatar Hugo Herbelin2016-10-19
| | | * [pp] Try to properly tag error messages in cError.Gravatar Emilio Jesus Gallego Arias2016-10-18
| |_|/ |/| |
| * | Removing output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-18
* | | Fixing a few other inconsistencies with notations.Gravatar Hugo Herbelin2016-10-17
* | | Fix output test for module qualification.Gravatar Pierre-Marie Pédrot2016-10-17
* | | Merge PR #310 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
|\| | | |/ |/|
| * Test for bug #4874.Gravatar Pierre-Marie Pédrot2016-10-17
* | Fix bug #4661: Cannot mask the absolute name.Gravatar Pierre-Marie Pédrot2016-10-01
* | Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\|
| * Fix test-suite.Gravatar Maxime Dénès2016-09-30
* | Ignore file names in warning emitted by test-suite/output/* (#5111)Gravatar Enrico Tassi2016-09-30
* | Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\|
* | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| * Fix a bug in subst releaved by an OCaml warning.Gravatar Maxime Dénès2016-09-29
* | Argument : assert does fail if no arg is given (fix #4864)Gravatar Enrico Tassi2016-09-29
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
|\|
| * Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Gravatar Hugo Herbelin2016-09-12
* | Merge remote-tracking branch 'github-coq/pr/249' into v8.6Gravatar Matthieu Sozeau2016-09-12
|\ \
| * | no-refold patchGravatar Paul Steckler2016-09-09
* | | Fix output test-suite after commit 0d3c319.Gravatar Pierre-Marie Pédrot2016-09-09
|/ /
* | Fixing output test-suite after warning for inner Requires.Gravatar Pierre-Marie Pédrot2016-08-30
| * Fix Errors.out missing a dot...Gravatar Matthieu Sozeau2016-07-19
* | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
* | Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
* | Fixing missing parentheses in printing of patterns in binders.Gravatar Hugo Herbelin2016-07-19
* | Notations: fixing multiple binders used as terms in reverse order.Gravatar Hugo Herbelin2016-07-19
* | Removing a source of clash with multiple recursive patterns in notations.Gravatar Hugo Herbelin2016-07-19
* | A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
* | Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
* | More examples of recursive notations, with emphasis in reference manual.Gravatar Hugo Herbelin2016-07-17
* | Fixing a bug in recognizing a recursive pattern of notationsGravatar Hugo Herbelin2016-07-17
* | Fixing interpretation of notations w/ opposite instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
* | Fixing printing of notations with several instances of a recursive pattern.Gravatar Hugo Herbelin2016-07-17
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-07-13
|\|
| * Fixing printing of evar name in an error message of instantiate.Gravatar Hugo Herbelin2016-07-13
* | Fix issues in test-suite revealed by warnings.Gravatar Maxime Dénès2016-06-29
* | Adding a test-suite for the only printing flag.Gravatar Pierre-Marie Pédrot2016-06-28
* | Patterns in binders: printing testsGravatar Arnaud Spiwack2016-06-27
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* | Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Gravatar Hugo Herbelin2016-06-24