1 files changed, 2 insertions, 2 deletions
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 0aca9a758b..f61999362f 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -22,12 +22,12 @@ Ltac compute_POS :=
   match goal with
   |  |- context [(Zpos (xI ?X1))] =>
       match constr:X1 with
-      | context [1%positive] => fail
+      | context [1%positive] => fail 1
       | _ => rewrite (BinInt.Zpos_xI X1)
       end
   |  |- context [(Zpos (xO ?X1))] =>
       match constr:X1 with
-      | context [1%positive] => fail
+      | context [1%positive] => fail 1
       | _ => rewrite (BinInt.Zpos_xO X1)
       end
   end.