diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-10-23 19:31:52 +0200 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-10-23 15:00:57 -0400 |
| commit | acc4c4601efd15aa6e6d8624ce7f9ccc08792177 (patch) | |
| tree | 6f3442895df07d1ed497817ffd7856a219a52319 /src/Util | |
| parent | 4b8ff5478b367cce44c87d5e3ecd94ff37593d57 (diff) | |
Tactic-in-term: ensuring same scope for all occurrences of a notation variable.
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 980dc4103..d4285a17a 100644 --- a/src/Util/SideConditions/ReductionPackages.v +++ b/src/Util/SideConditions/ReductionPackages.v @@ -39,7 +39,7 @@ Notation None_evar_Prop_package := (@None_evar_Prop_package' unit). Notation optional_evar_package pkg_type := (optional_evar_Prop_package - (ltac:(lazymatch eval hnf in pkg_type with evar_Prop_package ?P => exact P end)) + (ltac:(lazymatch eval hnf in pkg_type%type with evar_Prop_package ?P => exact P end)) pkg_type) (only parsing). |