diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-02-17 15:51:11 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-02-17 15:51:11 -0500 |
| commit | 3a52541b437413b5a142d8bdab6ce4f999358a4d (patch) | |
| tree | ba7dea55db0a71cbbf499376ceb89bf849637ecb /src/Util/Option.v | |
| parent | 46925caea4e63b3eabc328248e1a51e8728125c8 (diff) | |
Fix a proof for Coq 8.7
Diffstat (limited to 'src/Util/Option.v')
| -rw-r--r-- | src/Util/Option.v | 5 |
1 files changed, 3 insertions, 2 deletions
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) |