diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-10-31 15:10:42 +0100 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-11-01 15:02:56 -0400 |
| commit | 926dde9aea619ff983a43aa7161dabcfeb3c100e (patch) | |
| tree | 0a43e8ecdfdadea4c6ae173bc043e35b677797af /src/Util | |
| parent | fffdb8644bebe2e8ad9180f9680173476ea2b66d (diff) | |
Tactic-in-term: ensuring same scope for all occurrences of a notation variable.
Follow-up of acc4c460.
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/SideConditions/ReductionPackages.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/SideConditions/ReductionPackages.v b/src/Util/SideConditions/ReductionPackages.v index d4285a17a..61d4ef33a 100644 --- a/src/Util/SideConditions/ReductionPackages.v +++ b/src/Util/SideConditions/ReductionPackages.v @@ -57,7 +57,7 @@ Notation optional_evar_rel_package pkg_type x x _ (fun a b - => ltac:(lazymatch eval hnf in (pkg_type b) with + => ltac:(lazymatch eval hnf in (pkg_type%function b) with | evar_Prop_package ?P => let P := (eval cbv beta in (P a)) in exact P |