aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/TestRefine.v
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing TestRefine test-suite file.Gravatar Pierre-Marie Pédrot2014-09-08
* Fix the refine related test-suite files to account for the new refine.Gravatar Arnaud Spiwack2013-12-06
* Updating headers.Gravatar herbelin2012-08-08
* Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.Gravatar ppedrot2012-06-12
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Slight change of the semantics of user-given casts: they don't reallyGravatar msozeau2008-11-07
* Correction du bug 808: il est maintenant interdit de déclarer une assomption...Gravatar coq2006-03-02
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* Activation du test de Refine en v7 pour mémoire avant passage à la v8Gravatar herbelin2005-12-21