aboutsummaryrefslogtreecommitdiff
path: root/test-suite/misc
AgeCommit message (Expand)Author
2017-06-11A stronger test that #use"include";; works well.Hugo Herbelin
2017-05-10Moving code for miscellaneous tests to specific files.Hugo Herbelin
2017-05-10Adding tests for testing exit status and #use"include".Hugo Herbelin
2017-05-10Cleaning old untested not any more interesting testing files.Hugo Herbelin
2016-07-04test-suite: test checking of libraries checksum.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2011-12-19test suite update after r14808pboutill
2011-01-25Add a test for sorting all universes of stdlibglondu
2010-09-18Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-26Fixing xml theory file export (was not consistent with coqdoc fileherbelin