From 7146036f5a4555840a75b1fb564ee3c1b54623dc Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 11 May 2017 13:38:47 -0400
Subject: s/appcontext/context/

They mean the same thing since 8.5, and appcontext is deprecated.
---
 src/Util/WordUtil.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/Util/WordUtil.v')

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 839defb03..4b19d5f8b 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -953,7 +953,7 @@ Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordTo
 Proof.
   unfold wfirstn.
   intros; rewrite wordToNat_split1.
-  match goal with |- appcontext[match ?x with _ => _ end] => generalize x end.
+  match goal with |- context[match ?x with _ => _ end] => generalize x end.
   intro H'; destruct H'.
   reflexivity.
 Qed.
-- 
cgit v1.2.3