From 12e5ff9e4cfb7725fab450072c1a825e664a1395 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 15 Dec 2016 01:04:43 -0500
Subject: Fix 8.4 issues

---
 src/Reflection/Application.v       | 1 +
 src/Reflection/ApplicationLemmas.v | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/Reflection/Application.v b/src/Reflection/Application.v
index 3ddb25e1f..59e00ef1d 100644
--- a/src/Reflection/Application.v
+++ b/src/Reflection/Application.v
@@ -190,6 +190,7 @@ Arguments remove_binders {_} !_ !_ / .
 Arguments Apply {_ _ _ _ _ _} _ _ , {_ _ _} _ {_ _} _ _.
 Arguments Apply _ _ _ !_ _ _ !_ !_ / .
 Arguments ApplyInterped {_ _ !_ !_} _ _ / .
+Arguments ApplyInterped' {_ _} _ {_} _ _.
 Arguments ApplyAll {_ _ _ _ !_} !_ _ / .
 Arguments ApplyInterpedAll' {_ _ !_} _ _ / .
 Arguments ApplyInterpedAll {_ _ !_} _ _ / .
diff --git a/src/Reflection/ApplicationLemmas.v b/src/Reflection/ApplicationLemmas.v
index 9303ed378..f39e03776 100644
--- a/src/Reflection/ApplicationLemmas.v
+++ b/src/Reflection/ApplicationLemmas.v
@@ -39,7 +39,7 @@ Section language.
     : snd_binder (interp_all_binders_for_of' args) = interp_all_binders_for_of' (snd args).
   Proof.
     destruct B.
-    { edestruct interp_all_binders_for_of'; reflexivity. }
+    { destruct args as [? []]; reflexivity. }
     { destruct args; reflexivity. }
   Qed.
 
-- 
cgit v1.2.3