diff options
Diffstat (limited to 'src/Util/WordUtil.v')
| -rw-r--r-- | src/Util/WordUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |