aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
diff options
context:
space:
mode:
authorJason Gross <jagro@google.com>2016-08-01 12:48:35 -0700
committerJason Gross <jagro@google.com>2016-08-01 12:48:45 -0700
commitb92653291b6ac977d2bf1b72420d686580adf2f4 (patch)
tree0ea3b2f1122b71e4dc780f0d507597abe8861434 /src/Util/Equality.v
parent6c2cea42919f4b9754d7d748f6f8729468dbdf44 (diff)
Fixes for Coq 8.4
Diffstat (limited to 'src/Util/Equality.v')
-rw-r--r--src/Util/Equality.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 733b145c6..7657f96cb 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -41,7 +41,7 @@ Section gen.
Proof.
destruct H.
unfold decode.
- edestruct decode'.
+ edestruct (@decode' x _).
reflexivity.
Defined.
@@ -73,6 +73,6 @@ Section hprop.
intros x y p q.
pose proof (is_left_inv (@hprop_encode x y)) as H'.
rewrite <- (H' p), <- (H' q).
- apply f_equal, allpath_hprop.
+ apply f_equal; apply allpath_hprop.
Qed.
End hprop.