From c3b5ca7801220e3756136596b24e61ed66f34f10 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 31 Aug 2016 15:06:03 -0700 Subject: Add congruence_option tactic --- src/Util/Option.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'src/Util/Option.v') 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. -- cgit v1.2.3