diff options
| author |  Jason Gross <jagro@google.com> | 2016-08-31 15:06:03 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-08-31 15:06:03 -0700 |
| commit | c3b5ca7801220e3756136596b24e61ed66f34f10 (patch) | |
| tree | 814917117576882e1e1543619a77fd48d5c471ac /src/Util/Option.v | |
| parent | b28e23553230d08957af24a9a92d3c12a135a6ea (diff) | |
Add congruence_option tactic
Diffstat (limited to 'src/Util/Option.v')
| -rw-r--r-- | src/Util/Option.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Util/Option.v b/src/Util/Option.v index 2c11771ff..86e9a6d4f 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -69,3 +69,11 @@ Definition option_eq {A} eq (x y : option A) := | Some ay => eq ax ay end end. + +Ltac congruence_option := + repeat match goal with + | [ H : Some _ = Some _ |- _ ] => inversion H; clear H + | [ H : None = Some _ |- _ ] => solve [ inversion H ] + | [ H : Some _ = None |- _ ] => solve [ inversion H ] + | [ H : None = None |- _ ] => clear H + end. |