aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
AgeCommit message (Expand)Author
2017-06-09Fix Bug #5568, no dup notation warnings on repeated module importsPaul Steckler
2017-05-29Merge PR#546: Fix for bug #4499 and other minor related bugsMaxime Dénès
2017-05-28Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchMaxime Dénès
2017-05-26Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if prin...Maxime Dénès
2017-05-25Bug 5546, qualify datatype constructors when neededPaul Steckler
2017-05-19add test for Show with -emacs, bug 5535Paul Steckler
2017-05-17Fixing bug #5526,allow nonlinear variables in Notation patternsPaul Steckler
2017-05-01remove unneeded -emacs flag to coq-prog-argsPaul Steckler
2017-04-07Better support for printing constructors with let-ins.Hugo Herbelin
2017-04-07Fixing #4499 (not using unnamed record field in {| |} notation).Hugo Herbelin
2017-04-03Instances should obey universe binders even when defined by tactics.Gaetan Gilbert
2017-03-29Run non-tactic comands without resilient_commandTej Chajed
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 05:14:34 +0000