diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-01-26 11:56:59 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-01-26 11:56:59 +0000 |
| commit | f62060afc35df63ea0241bdc419623c814ab3941 (patch) | |
| tree | accbf827a13d72dfbd61c49bcd65c73eebe4ef54 | |
| parent | ece46e22da61e8a8d40766c533bcf2dd760deccb (diff) | |
| download | vericert-kvx-f62060afc35df63ea0241bdc419623c814ab3941.tar.gz vericert-kvx-f62060afc35df63ea0241bdc419623c814ab3941.zip | |
Add destruction to context match expressions
| -rw-r--r-- | src/common/Vericertlib.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 4f6c6fa..f2754be 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -73,9 +73,12 @@ Ltac solve_by_invert := solve_by_inverts 1. Ltac invert x := inversion x; subst; clear x. Ltac destruct_match := - match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? end. + match goal with + | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? + | [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:? + end. -Ltac auto_destruct x := destruct_with_eqn x; simpl in *; try discriminate; try congruence. +Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence. Ltac nicify_hypotheses := repeat match goal with |