Merge pull request #78 from SkySkimmer/intuit-auto

Stop using auto with * in intuition
coq-community · Jul 5, 2023 · 38faaaa · 38faaaa
2 parents a8c50a5 + 98cc80e
commit 38faaaa
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/BigQ/QMake.v b/BigQ/QMake.v
@@ -430,7 +430,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  Proof.
  intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl.
  rewrite Pos.mul_1_r, Z2Pos.id; auto.
- rewrite Z.mul_eq_0 in *; intuition.
+ rewrite Z.mul_eq_0 in *; intuition lia.
  nsubst; auto with zarith.
  nsubst; auto with zarith.
  nsubst; nzsimpl; auto with zarith.