diff options
| -rw-r--r-- | CHANGES | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -124,6 +124,10 @@ Tactics has been cleared or renamed in the current goal context now fail (possible source of incompatibilities solvable by avoiding clearing the relevant hypotheses). +- Tactic "constructor" is now fully backtracking, thus deprecating the need of + the undocumented "contructor <tac>" syntax which is now equivalent to + "once (constructor; tac)". (potential source of rare incompatibilities). + Program |
