blob: 09bef82c8012e0b44668f480aa6b674c6c8bb42f (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now
only run their tactic argument once, even if it has multiple
successes. This prevents blow-up and looping from using
multisuccess tactics with :tacn:`assert_succeeds`. (`#10966
<https://github.com/coq/coq/pull/10966>`_ fixes `#10965
<https://github.com/coq/coq/issues/10965>`_, by Jason Gross).
- The :tacn:`assert_succeeds` and :tacn:`assert_fails` tactics now
behave correctly when their tactic fully solves the goal. (`#10966
<https://github.com/coq/coq/pull/10966>`_ fixes `#9114
<https://github.com/coq/coq/issues/9114>`_, by Jason Gross).
|
