From 85aa93d4a986ec8560dc07ddd861a0820c713eec Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 16 Nov 2016 08:20:56 +0100
Subject: [PATCH] Replace deprecated appcontext -> context.
---
theories/option.v | 8 ++++----
theories/tactics.v | 4 ++--
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/theories/option.v b/theories/option.v
index 7e5da6e5..16eee71f 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -298,11 +298,11 @@ End union_intersection_difference.
(** * Tactics *)
Tactic Notation "case_option_guard" "as" ident(Hx) :=
match goal with
- | H : appcontext C [@mguard option _ ?P ?dec] |- _ =>
+ | H : context C [@mguard option _ ?P ?dec] |- _ =>
change (@mguard option _ P dec) with (λ A (f : P → option A),
match @decide P dec with left H' => f H' | _ => None end) in *;
destruct_decide (@decide P dec) as Hx
- | |- appcontext C [@mguard option _ ?P ?dec] =>
+ | |- context C [@mguard option _ ?P ?dec] =>
change (@mguard option _ P dec) with (λ A (f : P → option A),
match @decide P dec with left H' => f H' | _ => None end) in *;
destruct_decide (@decide P dec) as Hx
@@ -326,9 +326,9 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
assert (mx = Some x') as H by tac
| assert (mx = None) as H by tac ]
in repeat match goal with
- | H : appcontext [@mret _ _ ?A] |- _ =>
+ | H : context [@mret _ _ ?A] |- _ =>
change (@mret _ _ A) with (@Some A) in H
- | |- appcontext [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
+ | |- context [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
| H : context [mbind (M:=option) (A:=?A) ?f ?mx] |- _ =>
let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
| H : context [fmap (M:=option) (A:=?A) ?f ?mx] |- _ =>
diff --git a/theories/tactics.v b/theories/tactics.v
index 583b544f..e0283a9e 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -158,7 +158,7 @@ Coq-club message:
https://sympa.inria.fr/sympa/arc/coq-club/2012-10/msg00147.html *)
Ltac fold_classes :=
repeat match goal with
- | |- appcontext [ ?F ] =>
+ | |- context [ ?F ] =>
progress match type of F with
| FMap _ =>
change F with (@fmap _ F);
@@ -176,7 +176,7 @@ Ltac fold_classes :=
end.
Ltac fold_classes_hyps H :=
repeat match type of H with
- | appcontext [ ?F ] =>
+ | context [ ?F ] =>
progress match type of F with
| FMap _ =>
change F with (@fmap _ F) in H;
--
GitLab