diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-08-01 11:51:30 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 11:47:51 -0400 |
commit | 9485009e21f65381286d8e88903e0360c04f3cc5 (patch) | |
tree | a0710be5d7943c5989defba8fb4f0d32cf3a4808 /src | |
parent | 333f867f010eb00db777916d4ee757f9ff2216b4 (diff) |
Util.Equality on 8.4
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/Equality.v | 2 |
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. |