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
/
induct.v
Commit message (
Expand
)
Author
Age
*
Update headers.
Maxime Dénès
2015-01-12
*
Preserving the good effect of 014e5ac92a on not leaving dangling local
Hugo Herbelin
2014-11-14
*
Compatibility with 8.4 in the heuristic used to build the induction
Hugo Herbelin
2014-11-08
*
Some reorganization of the code for destruct/induction:
Hugo Herbelin
2014-11-02
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Synchronized names from the "as" clause with the skeleton of the
Hugo Herbelin
2014-06-30
*
Updating headers.
herbelin
2012-08-08
*
Restore test file induct.v where the "in |- *" is mandatory
letouzey
2012-07-10
*
Kills the useless tactic annotations "in |- *"
letouzey
2012-07-05
*
"Let in" in pattern hell, one more iteration
pboutill
2012-03-02
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.
herbelin
2009-09-27
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Ensures that let-in's in arities of inductive types work well. Maybe not
herbelin
2009-08-11
*
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
herbelin
2005-12-21
*
Nouvelle en-tête
herbelin
2004-07-16
*
entetes
filliatr
2001-03-15
*
Ajout de tests
mohring
2000-12-12