diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-09 17:18:17 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-09 17:18:17 +0000 |
| commit | fbc0242a1d9c280de22da165c162ef24e4981ff1 (patch) | |
| tree | defdfb25b26dbf98b080583613551fb658295ff4 /CHANGES | |
| parent | 5f547a9465e629d30ecce3da74090334dbdb63bf (diff) | |
New version of Functional Scheme and functional induction. Deals with
more functions (higher order and polymorphic functions), the principle
is a bit better.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5310 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -141,6 +141,8 @@ Vernacular commands and on substrings of the name of the lemma - "Print Implicit" displays the implicit arguments of a constant - Locate now searches for all names having a given suffix +- New command "Functional Scheme" for building an induction principle + from a function defined by case analysis and fix. Commands @@ -226,6 +228,8 @@ Tactics immediate hint), resulting in shorter proofs - Instantiate now works in hyps (syntax : Instantiate in ...) - Some new tactics : EConstructor, ELeft, Eright, ESplit, EExists +- New tactic "functional induction" to perform case analysis and + induction following the definition of a function. - Clear now fails when trying to remove a local definition used by a constant appearing in the current goal |