diff options
| -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. |