From e3dd9ae19ea08b8cbe3c6532ffb6b4d4e3e2ab38 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 18 Apr 2018 15:38:27 -0400 Subject: Change a proof in src/Util/Option This was causing issues with bug minimization because some hints seem to follow [Require], not [Import], and so when [eauto] got stronger, this proof was failing. --- src/Util/Option.v | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'src/Util/Option.v') diff --git a/src/Util/Option.v b/src/Util/Option.v index e04ae12dd..96014448b 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -66,10 +66,8 @@ Lemma option_rect_false_returns_true_iff (f:T->bool) {Proper_f:Proper(R==>eq)f} (o:option T) : option_rect (fun _ => bool) f false o = true <-> exists s:T, option_eq R o (Some s) /\ f s = true. Proof. - unfold option_rect; break_match; repeat intuition (destruct_head ex; eauto); [ | | congruence.. ]. + unfold option_rect; break_match; repeat intuition (destruct_head ex; eauto); try discriminate. { repeat esplit; simpl; easy. } - { match goal with [H : f _ = true |- f _ = true ] => - solve [rewrite <- H; eauto] end. } Qed. Lemma option_rect_false_returns_true_iff_eq -- cgit v1.2.3