diff options
| author | Hugo Herbelin | 2014-07-13 17:47:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-07-13 18:02:57 +0200 |
| commit | c2b0ca88cbc4e874e7b3bd9b9f4c07477cb5b530 (patch) | |
| tree | d0e03a08be41eda0bb7fab325e3e5160dc2e273a | |
| parent | d29b487f7c50fd8332cb1cfc144f70bc7db595d9 (diff) | |
Mentioning the incompatibility due to fixing bug #2996 (see #3418).
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -120,6 +120,10 @@ Tactics - Tactic "subst id" now supports id occurring in dependent local definitions. - Bugs fixed about intro-pattern "*" might lead to some rare incompatibilities. - New tactical "time" to display time spent executing its argument. +- Tactics referring or using a constant dependent in a section variable which + has been cleared or renamed in the current goal context now fail + (possible source of incompatibilities solvable by avoiding clearing + the relevant hypotheses). Program |