From 9485009e21f65381286d8e88903e0360c04f3cc5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 1 Aug 2016 11:51:30 -0400 Subject: Util.Equality on 8.4 --- src/Util/Equality.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util/Equality.v') 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. -- cgit v1.2.3