aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/Funind.v
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2006-07-04functional inversion now takes a quatified hypothesis as first argumentjforest
2006-07-04- completely new version of "functional inversion" using inversion onjforest
2006-06-23modifs de test-suite suite au passage des graphes de Function dans Typejforest
2006-06-06+ ameliorating the tactic "functional induction"jforest
2005-12-21Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8herbelin
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
2003-06-21Added a test for Functional Induction.courtieu
2003-02-28fixing a typo in the new Funinv.v test in test-suite/successcourtieu
2003-02-27Adding tests for the "functional induction" facility.bertot