From 7fd387e4ac13e38620ad480afafeca53caa7dabb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 16 Sep 2016 18:10:30 -0700 Subject: Fix for Coq 8.5 --- 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 98e172ad4..03fd77988 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -16,7 +16,7 @@ Global Instance Equivalence_option_eq {T} {R} {Equivalence_R:@Equivalence T R} : Equivalence (option_eq R). Proof. split; cbv; repeat (break_match || intro || intuition congruence || - solve [ reflexivity | symmetry; eassumption | etransitivity; eassumption ] ). + solve [ apply reflexivity | apply symmetry; eassumption | eapply transitivity; eassumption ] ). Qed. -- cgit v1.2.3