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 | |
| parent | 0b0f75b427c8c95ac31a77b29725e6cd7fb16482 (diff) | |
Fix 8.4 issues
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Application.v | 1 | ||||
| -rw-r--r-- | src/Reflection/ApplicationLemmas.v | 2 |
2 files changed, 2 insertions, 1 deletions
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. |