aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2017-01-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2017-01-05Fixing a little bug in printing cofix with no arguments.Hugo Herbelin
2016-12-02Fix test-suite after change in "context" printing.Maxime Dénès
2016-11-10Updating a comment in test-suite.Hugo Herbelin
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-11-07Fix #5182: "Arguments names must be distinct." is bogus and underinformativeMaxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
2016-10-28Merge remote-tracking branch 'github/pr/337' into v8.6Maxime Dénès
2016-10-27Add missing dot to impargs error message.Maxime Dénès
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-24Adding a test for #4398 (interpretation scopes for "match goal").Hugo Herbelin
2016-10-22Merge branch 'v8.5' into v8.6Hugo Herbelin
2016-10-22Fixing printing of generic arguments of tag "var".Hugo Herbelin
2016-10-22Unification constraint handling (#4763, #5149)Matthieu Sozeau
2016-10-21Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Matthieu Sozeau
2016-10-20[search] Don't build intermediate lists in search.Emilio Jesus Gallego Arias
2016-10-19Test for variant of #5142 (good error message on pattern-matching failure).Hugo Herbelin
2016-10-19Attempt to improve error rendering in pattern-matching compilation (#5142).Hugo Herbelin
2016-10-18[pp] Try to properly tag error messages in cError.Emilio Jesus Gallego Arias
2016-10-18Removing output test for module qualification.Pierre-Marie Pédrot
2016-10-17Fixing a few other inconsistencies with notations.Hugo Herbelin
2016-10-17Fix output test for module qualification.Pierre-Marie Pédrot
2016-10-17Merge PR #310 into v8.6Pierre-Marie Pédrot
2016-10-17Test for bug #4874.Pierre-Marie Pédrot
2016-10-01Fix bug #4661: Cannot mask the absolute name.Pierre-Marie Pédrot
2016-09-30Merge branch 'v8.5' into v8.6Maxime Dénès
2016-09-30Fix test-suite.Maxime Dénès
2016-09-30Ignore file names in warning emitted by test-suite/output/* (#5111)Enrico Tassi
2016-09-30Merge branch 'v8.5' into v8.6Maxime Dénès
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-09-29Fix a bug in subst releaved by an OCaml warning.Maxime Dénès
2016-09-29Argument : assert does fail if no arg is given (fix #4864)Enrico Tassi
2016-09-14Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-12Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Hugo Herbelin
2016-09-12Merge remote-tracking branch 'github-coq/pr/249' into v8.6Matthieu Sozeau
2016-09-09no-refold patchPaul Steckler
2016-09-09Fix output test-suite after commit 0d3c319.Pierre-Marie Pédrot
2016-08-30Fixing output test-suite after warning for inner Requires.Pierre-Marie Pédrot
2016-07-19Fix Errors.out missing a dot...Matthieu Sozeau
2016-07-19Some extra fixes in printing patterns in binders.Hugo Herbelin
2016-07-19Taking into account binding patterns when agglutinating sequences of binders.Hugo Herbelin
2016-07-19Fixing missing parentheses in printing of patterns in binders.Hugo Herbelin
2016-07-19Notations: fixing multiple binders used as terms in reverse order.Hugo Herbelin
2016-07-19Removing a source of clash with multiple recursive patterns in notations.Hugo Herbelin
2016-07-18A new step on using alpha-conversion in printing notations.Hugo Herbelin
2016-07-17Partial fix to #4592 (notation requiring alpha-conversion for printing).Hugo Herbelin
2016-07-17More examples of recursive notations, with emphasis in reference manual.Hugo Herbelin
2016-07-17Fixing a bug in recognizing a recursive pattern of notationsHugo Herbelin
2016-07-17Fixing interpretation of notations w/ opposite instances of a recursive pattern.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 04:53:48 +0000