diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-12-15 01:04:43 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-12-15 01:04:43 -0500 |
| commit | 12e5ff9e4cfb7725fab450072c1a825e664a1395 (patch) | |
| tree | 70da2673e43c4f32f8ccdf7ce8e329bb30031bce /src/Reflection/ApplicationLemmas.v | |
| parent | 0b0f75b427c8c95ac31a77b29725e6cd7fb16482 (diff) | |
Fix 8.4 issues
Diffstat (limited to 'src/Reflection/ApplicationLemmas.v')
| -rw-r--r-- | src/Reflection/ApplicationLemmas.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |