From ad22d3d211bc84dd50cbd2259e5bb0a3fb735e88 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 18 Oct 2016 17:13:27 -0400 Subject: Fix for Coq 8.5, 8.5pl1 --- src/Util/Option.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/Util/Option.v') diff --git a/src/Util/Option.v b/src/Util/Option.v index 591a285ad..82ddf6750 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -12,22 +12,22 @@ Section Relations. | Some ay => eq ax ay end end. - + Local Ltac t := cbv; repeat (break_match || intro || intuition congruence || solve [ apply reflexivity | apply symmetry; eassumption | eapply transitivity; eassumption ] ). - + Global Instance Reflexive_option_eq {T} {R} {Reflexive_R:@Reflexive T R} : Reflexive (option_eq R). Proof. t. Qed. - + Global Instance Transitive_option_eq {T} {R} {Transitive_R:@Transitive T R} : Transitive (option_eq R). Proof. t. Qed. - + Global Instance Symmetric_option_eq {T} {R} {Symmetric_R:@Symmetric T R} : Symmetric (option_eq R). Proof. t. Qed. - + Global Instance Equivalence_option_eq {T} {R} {Equivalence_R:@Equivalence T R} : Equivalence (option_eq R). Proof. split; exact _. Qed. End Relations. @@ -52,7 +52,7 @@ Lemma option_rect_false_returns_true_iff option_rect (fun _ => bool) f false o = true <-> exists s:T, option_eq R o (Some s) /\ f s = true. Proof. unfold option_rect; break_match; logic; [ | | congruence .. ]. - { repeat esplit; easy. } + { repeat esplit; simpl; easy. } { match goal with [H : f _ = true |- f _ = true ] => solve [rewrite <- H; eauto] end. } Qed. -- cgit v1.2.3