diff options
| author | Hugo Herbelin | 2014-06-30 09:24:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-30 17:23:10 +0200 |
| commit | a0ccd7bdc29c35dd291a526891fdbb9909b8e827 (patch) | |
| tree | df984988850c92ffe32d0e57edfa482f931675ee /CHANGES | |
| parent | 1f0f842e92be66f67044bdc6deb70676f0ffc22f (diff) | |
Synchronized names from the "as" clause with the skeleton of the
elimination scheme in induction/destruct also for those names which
correspond to neither the induction hypotheses nor the recursive
arguments.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -118,6 +118,7 @@ Tactics the option "Set Injection On Proofs" (disabled by default). Also improved the error messages. - Tactic "subst id" now supports id occurring in dependent local definitions. +- Bugs fixed about intro-pattern "*" might lead to some rare incompatibilities. Program |