aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Wf.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program/Wf.v')
-rw-r--r--theories/Program/Wf.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index a2fd05cd9..c490ea516 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -211,7 +211,7 @@ Ltac fold_sub f :=
match goal with
| [ |- ?T ] =>
match T with
- appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] =>
+ context C [ @Fix_sub _ _ _ _ _ ?arg ] =>
let app := context C [ f arg ] in
change app
end