diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-21 13:43:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-01 12:05:39 +0100 |
| commit | 711b9d8cdf6e25690d247d9e8c49f005527e64e2 (patch) | |
| tree | 5a19ec52e7a510a456195d3814958abc33e47f73 /CHANGES | |
| parent | f726e860917b56abc94f21d9d5add7594d23bb6d (diff) | |
Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".
Noticed by Sigurd Schneider.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -54,6 +54,9 @@ Tactics with let bindings in the parameters. - The tactic "dtauto" now handles some inductives such as "@sigT A (fun _ => B)" as non-dependent conjunctions. +- A bug fixed in "rewrite H in *" and "rewrite H in * |-" may cause a + few rare incompatibilities (it was unintendedly recursively + rewriting in the side conditions generated by H). Focusing |