diff options
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 := |