aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics/SimplifyProjections.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/Tactics/SimplifyProjections.v')
-rw-r--r--src/Util/Tactics/SimplifyProjections.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/Tactics/SimplifyProjections.v b/src/Util/Tactics/SimplifyProjections.v
index f9b319057..bf9f2d347 100644
--- a/src/Util/Tactics/SimplifyProjections.v
+++ b/src/Util/Tactics/SimplifyProjections.v
@@ -8,7 +8,7 @@ Ltac pre_simplify_projection proj proj' uproj' :=
Ltac do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct :=
change proj' with uproj' at 1;
lazymatch goal with
- | [ |- appcontext[uproj' _ _ (construct _ _ _ _)] ]
+ | [ |- context[uproj' _ _ (construct _ _ _ _)] ]
=> cbv beta iota delta [uproj']
| _ => change uproj' with proj
end.