aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Record.v
Commit message (Expand)AuthorAge
* Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
* More precise on preventing clash between bound vars name and hidden impargs.Gravatar Hugo Herbelin2017-05-31
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
* Add some example uses of the new record features in Record.v:Gravatar msozeau2008-11-07
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21
* Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...Gravatar herbelin2003-01-15