From 926dde9aea619ff983a43aa7161dabcfeb3c100e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 31 Oct 2018 15:10:42 +0100 Subject: Tactic-in-term: ensuring same scope for all occurrences of a notation variable. Follow-up of acc4c460. --- src/Util/SideConditions/ReductionPackages.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Util') 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 -- cgit v1.2.3