Adapt w.r.t. coq/coq#15442.

coq-community · Jan 6, 2022 · ca0795c · ca0795c
1 parent 8f0f022
commit ca0795c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Programming/Show.v b/theories/Programming/Show.v
@@ -177,7 +177,7 @@ Section hiding_notation.
   Next Obligation.
     assert (NPeano.Nat.div n 10 < n) ; eauto.
     eapply NPeano.Nat.div_lt.
-    inversion H; apply Lt.lt_O_Sn.
+    match goal with [ H : n > _ |- _ ] => inversion H end; apply Lt.lt_O_Sn.
     repeat constructor.
   Defined.
   Global Instance nat_Show : Show nat := { show := nat_show }.