diff options
| -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 |