aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-07-18 00:53:38 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-07-18 00:57:24 +0200
commita07af57f3140a2481e1e2f45a930a17d80a33645 (patch)
tree5ea91c9bede1cbf1aa1991b7c3875fb20bedf8e5 /plugins
parentddf50c8bb15ce86fc3e3fbedf9f86fd278f01776 (diff)
Fix bug #4923: Warning: appcontext is deprecated.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/micromega/Env.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v
index a19e9df90..7e3ef8929 100644
--- a/plugins/micromega/Env.v
+++ b/plugins/micromega/Env.v
@@ -93,7 +93,7 @@ End S.
Ltac jump_simpl :=
repeat
match goal with
- | |- appcontext [jump xH] => rewrite (jump_simpl xH)
- | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p))
- | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p))
+ | |- context [jump xH] => rewrite (jump_simpl xH)
+ | |- context [jump (xO ?p)] => rewrite (jump_simpl (xO p))
+ | |- context [jump (xI ?p)] => rewrite (jump_simpl (xI p))
end.