diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-20 12:11:04 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-20 12:11:04 -0700 |
| commit | 8c999bd5229fde5ebd3a9f32ba5888309e144837 (patch) | |
| tree | e17d6fdbdd30e442e3613622ca7499177a6dabab /Bedrock | |
| parent | 817790844673724a13ccdbbf509e1d2885f4d293 (diff) | |
Silence a deprecation warning
Diffstat (limited to 'Bedrock')
| -rw-r--r-- | Bedrock/Word.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Bedrock/Word.v b/Bedrock/Word.v index 8ae651826..036b3198a 100644 --- a/Bedrock/Word.v +++ b/Bedrock/Word.v @@ -845,7 +845,7 @@ Proof. eapply weqb_true_iff. Qed. -Implicit Arguments weqb_sound []. +Arguments weqb_sound : clear implicits. Ltac isWcst w := match eval hnf in w with |