diff options
| author |  Jason Gross <jagro@google.com> | 2016-09-16 18:10:30 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-09-16 18:10:30 -0700 |
| commit | 7fd387e4ac13e38620ad480afafeca53caa7dabb (patch) | |
| tree | bd1477a416486bce99a0e77f4c40cd2ffba30533 /src/Util/Option.v | |
| parent | e28b498c98295b5e0f9873db4cbbe30957fb6e0b (diff) | |
Fix for Coq 8.5
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 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. |