Skip to content
Snippets Groups Projects
Commit 4f00de71 authored by Armaël Guéneau's avatar Armaël Guéneau
Browse files

Changelog entry

parent 1e9a5ae9
No related branches found
No related tags found
1 merge request!117Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption
...@@ -17,6 +17,13 @@ API-breaking change is listed. ...@@ -17,6 +17,13 @@ API-breaking change is listed.
- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma - Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma
`list_to_vec_to_list` for the converse. `list_to_vec_to_list` for the converse.
- Add `Countable` instance for `vec`. - Add `Countable` instance for `vec`.
- Introduce `destruct_or{?,!}` to repeatedly destruct disjunctions in
assumptions. The tactic can also be provided an explicit assumption name;
`destruct_and{?,!}` has been generalized accordingly and now can also be
provided an explicit assumption name.
Slight breaking change: `destruct_and` no longer handle `False`;
`destruct_or` now handles `False` while `destruct_and` handles `True`,
as the respective units of disjunction and conjunction.
## std++ 1.2.1 (released 2019-08-29) ## std++ 1.2.1 (released 2019-08-29)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment