From 356f43e29f1da80fb34035d72eeeadac238210d8 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 14 Dec 2016 13:37:07 -0500
Subject: Work around bug in 8.4 apply

---
 src/Util/Option.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/src/Util/Option.v b/src/Util/Option.v
index 64bdb4197..c67efcb1a 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -140,7 +140,7 @@ Qed.
 
 Lemma invert_eq_Some {A x y} (p : Some x = Some y) : { pf : x = y | @option_eq_to_leq A (Some x) (Some y) pf = p }.
 Proof.
-  eexists; apply option_leq_to_eq_to_leq.
+  refine (exist _ _ (option_leq_to_eq_to_leq _)).
 Qed.
 
 Ltac inversion_option_step :=
-- 
cgit v1.2.3