aboutsummaryrefslogtreecommitdiff
path: root/src/Util
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util')
-rw-r--r--src/Util/SideConditions/ReductionPackages.v2
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