From 8c999bd5229fde5ebd3a9f32ba5888309e144837 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 20 Jul 2016 12:11:04 -0700 Subject: Silence a deprecation warning --- Bedrock/Word.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Bedrock') 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 -- cgit v1.2.3