index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
success
/
Funind.v
Age
Commit message (
Expand
)
Author
2020-05-16
Fix #11761: Functional Induction throws unrecoverable error.
Pierre Courtieu
2017-06-14
Prelude : no more autoload of plugins extraction and recdef
Pierre Letouzey
2014-07-11
Fix Funind test-suite file after patch by Pierre.
Matthieu Sozeau
2014-05-06
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
2012-07-05
Kills the useless tactic annotations "in |- *"
letouzey
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2006-07-04
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-06-23
modifs de test-suite suite au passage des graphes de Function dans Type
jforest
2006-06-06
+ ameliorating the tactic "functional induction"
jforest
2005-12-21
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2004-02-09
New version of Functional Scheme and functional induction. Deals with
coq
2003-06-21
Added a test for Functional Induction.
courtieu
2003-02-28
fixing a typo in the new Funinv.v test in test-suite/success
courtieu
2003-02-27
Adding tests for the "functional induction" facility.
bertot
