aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Bedrock/Word.v2
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