From 3a52541b437413b5a142d8bdab6ce4f999358a4d Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 17 Feb 2018 15:51:11 -0500
Subject: Fix a proof for Coq 8.7

---
 src/Util/Option.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/Util/Option.v')

diff --git a/src/Util/Option.v b/src/Util/Option.v
index 59fd65ca3..e04ae12dd 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -222,8 +222,9 @@ Qed.
 Lemma bind_neq_None_iff' {A B} (x : option A) (f : A -> option B)
   : (bind x f <> None) <-> (exists pf : x <> None, f (@always_invert_Some _ x pf) <> None).
 Proof.
-  destruct x as [x|]; cbn; [ destruct (f x); cbn | ]; repeat dintuition (congruence || constructor || eauto).
-  match goal with H : ex _ |- _ => destruct H end; congruence.
+  destruct x as [x|]; cbn; [ destruct (f x); cbn | ];
+    split; intros; destruct_head'_ex; try unshelve econstructor;
+      congruence.
 Qed.
 
 Definition push_always_invert_Some_bind {A B} (x : option A) (f : A -> option B)
-- 
cgit v1.2.3