Skip to content

Commit 159c361

Browse files
authored
Use replace instead of cutrewrite. (#101)
Compatibility with rocq-prover/rocq#12993.
1 parent 33bb328 commit 159c361

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

theories/Data/ListFirstnSkipn.v

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ Lemma firstn_cons : forall T n a (b : list T),
4141
Proof.
4242
destruct n; intros.
4343
omega.
44-
simpl. cutrewrite (n - 0 = n); [ | omega ]. reflexivity.
44+
simpl. replace (n - 0) with n; [ | omega ]. reflexivity.
4545
Qed.
4646

4747
Hint Rewrite firstn_app_L firstn_app_R firstn_all firstn_0 firstn_cons using omega : list_rw.
@@ -86,7 +86,7 @@ Lemma skipn_cons : forall T n a (b : list T),
8686
Proof.
8787
destruct n; intros.
8888
omega.
89-
simpl. cutrewrite (n - 0 = n); [ | omega ]. reflexivity.
89+
simpl. replace (n - 0) with n; [ | omega ]. reflexivity.
9090
Qed.
9191

92-
Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using omega : list_rw.
92+
Hint Rewrite skipn_app_L skipn_app_R skipn_0 skipn_all skipn_cons using omega : list_rw.

0 commit comments

Comments
 (0)