diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-12-14 13:37:07 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-12-14 13:37:07 -0500 |
| commit | 356f43e29f1da80fb34035d72eeeadac238210d8 (patch) | |
| tree | 2c7b6cf7fdece531b0569b00149077e12be4b55a /src/Util/Option.v | |
| parent | 0901e4b43842c6b0266bb796c842cbcc21880776 (diff) | |
Work around bug in 8.4 apply
Diffstat (limited to 'src/Util/Option.v')
| -rw-r--r-- | src/Util/Option.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 := |