aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-08-01 11:51:30 -0400
committerGravatar Andres Erbsen <andreser@mit.edu>2016-08-04 11:47:51 -0400
commit9485009e21f65381286d8e88903e0360c04f3cc5 (patch)
treea0710be5d7943c5989defba8fb4f0d32cf3a4808 /src
parent333f867f010eb00db777916d4ee757f9ff2216b4 (diff)
Util.Equality on 8.4
Diffstat (limited to 'src')
-rw-r--r--src/Util/Equality.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 3c3ddd9ff..b128305f0 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -73,7 +73,7 @@ Section gen.
Proof.
destruct H.
unfold decode.
- edestruct (@decode' x _).
+ edestruct (decode' (encode x eq_refl)).
reflexivity.
Defined.