index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
success
/
Funind.v
Commit message (
Expand
)
Author
Age
*
Fix Funind test-suite file after patch by Pierre.
Matthieu Sozeau
2014-07-11
*
Comment in Funind.v test-suite file
Matthieu Sozeau
2014-05-06
*
- Fixes for canonical structure resolution (check that the initial term indee...
Matthieu Sozeau
2014-05-06
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
functional inversion now takes a quatified hypothesis as first argument
jforest
2006-07-04
*
- completely new version of "functional inversion" using inversion on
jforest
2006-07-04
*
modifs de test-suite suite au passage des graphes de Function dans Type
jforest
2006-06-23
*
+ ameliorating the tactic "functional induction"
jforest
2006-06-06
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
New version of Functional Scheme and functional induction. Deals with
coq
2004-02-09
*
Added a test for Functional Induction.
courtieu
2003-06-21
*
fixing a typo in the new Funinv.v test in test-suite/success
courtieu
2003-02-28
*
Adding tests for the "functional induction" facility.
bertot
2003-02-27