Adapt to math-comp/math-comp#1223

coq-community · Jun 28, 2024 · cc6ee10 · cc6ee10
1 parent 07cbbe8
commit cc6ee10
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/theories/schutte/ssete9.v b/theories/schutte/ssete9.v
@@ -1918,7 +1918,7 @@ Lemma mul_int n m : \F n * \F m = \F (n *m)%N.
 Proof.
 case: n; first by rewrite T1mul0n.
 move => n;case: m; first by rewrite T1muln0 muln0.
-by move => m /=; rewrite - mulnE mulnSr addnC.
+by move=> m /=; rewrite -?mulnE mulnSr addnC.  (* FIXME: remove -?mulnE when requiring Coq >= 8.21 *)
 Qed.
 
 Lemma mul_phi0 a b: phi0 (a + b) = phi0 a * phi0 b.
@@ -3780,7 +3780,7 @@ Lemma T2addn0: right_id zero T2add.    Proof. by case. Qed.
 
 Lemma add_int n m : \F n + \F m = \F (n +m)%N.
 Proof.
-by case: n m => // n [ | m]; rewrite /= - ? addnS  // - addnE addn0.
+by case: n m => // n [ | m]; rewrite /= - ? addnS  // -?addnE addn0.  (* FIXME: remove -?addnE when requiring Coq >= 8.21 *)
 Qed.
 
 Lemma add_fin_omega n: \F n + omega = omega.

diff --git a/theories/stern/fibm.v b/theories/stern/fibm.v
@@ -3965,7 +3965,7 @@ apply:ZeckM_prop3; apply/andP; split.
    by elim:n (0) => // k H n /=; rewrite H eqxx.
 rewrite  /Zeck_val - fib_sum !big_ord_recl /=.
 elim:n => [|n Hr];first by rewrite big_nil big_ord0.
-by rewrite big_ord_recr - (eqP Hr) iota_Sr rev_rcons big_cons addnC.
+by rewrite big_ord_recr 1?addnA -(eqP Hr) iota_Sr rev_rcons big_cons addnC.  (* FIXME: change 1?addnA into addnA when requiring Coq >= 8.21 *)
 Qed.