aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/RecTutorial.v
Commit message (Expand)AuthorAge
* Introduce an option to allow nested lemma, and turn it off by default.Gravatar Théo Zimmermann2018-05-17
* Change Implicit Arguments to Arguments in test-suiteGravatar Jasper Hugunin2018-03-30
* Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
* Test-suite fix to 1744e37 (injection in context).Gravatar Hugo Herbelin2016-06-18
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* - Fix RecTutorial, and mutual induction schemes getting the wrong names.Gravatar Matthieu Sozeau2014-05-06
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Fix the test-suite by removing any Reset in the scriptsGravatar letouzey2012-03-23
* Some fixes of the test-suite scriptsGravatar letouzey2011-02-21
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Adaptation au passage de vector dans TypeGravatar herbelin2006-05-28
* Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...Gravatar herbelin2006-01-23
* Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8Gravatar herbelin2005-12-21