diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-04 19:50:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-04 19:50:44 +0100 |
| commit | fdea9174359868bd9d4f3cf397243c0be921f0d8 (patch) | |
| tree | 36430caf6f81cb49ea5a7a10716523f7df9f4290 /CHANGES | |
| parent | bcba6d1bc9f769da593a3b01a12846f3e7a26a25 (diff) | |
Documenting the change of semantics of the replace tactic.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -217,6 +217,7 @@ Tactics - non-dependent destruct/induction on an hypothesis with premisses in an inductive type with indices is fixed - residual local definitions are now correctly removed. +- The replace tactic may now replace variables in parallel. Program |