aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coqdoc
AgeCommit message (Expand)Author
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...Maxime Dénès
2017-11-13Fixing encoding in coqdoc output tests.Hugo Herbelin
2017-11-08Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.Hugo Herbelin
2017-10-05Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Hugo Herbelin
2017-08-29coqdoc: Support comments in verbatim outputTej Chajed
2017-07-19Removing testing unsupported Next.Hugo Herbelin
2017-07-17Adding a coqdoc target to test-suite.Hugo Herbelin
2010-04-06New model for user-driven translation of tokens in coqdocherbelin
2010-03-30Small things about coqdoc + fixing lettuple.v test (part of bug #2289)herbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin