Require Coq 8.12

refinedc.opam

@@ -16,7 +16,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/refinedc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/iris/refinedc.git"
 
 depends: [
-  "coq" { (>= "8.11.0" & < "8.12~") }
+  "coq" { (>= "8.12.0" & < "8.13~") }
   "coq-iris" { (= "dev.2020-10-01.3.8f6c063a") | (= "dev") }
   "dune" {>= "2.7.0"}
   "cerberus" {= "~dev"}

theories/lang/base.v

@@ -379,7 +379,7 @@ Definition keep_factor2 (n : nat) (def : nat) : nat :=
 
 Lemma Pos_pow_add_r a b c:
   (a ^ (b + c) = a ^ b * a ^ c)%positive.
-Proof. zify. rewrite !Pos2Z.inj_pow Pos2Z.inj_add Z.pow_add_r; lia. Qed.
+Proof. zify. rewrite Z.pow_add_r; lia. Qed.
 
 Lemma Pos_factor2_mult_xI a b:
   Pos_factor2 (a~1 * b) = Pos_factor2 b.

theories/lithium/simpl_instances.v

@@ -93,7 +93,6 @@ Proof.
   unfold CanSolve in *. rewrite /Z.divide. split.
   - move => HT [x Hx]. apply: (HT (Z.to_nat x)).
     rewrite -Z2Nat.inj_mul; try lia.
-    apply (Z.mul_nonneg_cancel_r _ a); lia.
   - move => HT n ?. apply HT. eexists n. lia.
 Qed.