Skip to content

Commit 4f8f2b1

Browse files
proux01xavierleroy
andauthored
Avoid using is as a variable name
`is` might become reserved soon because of rocq-prover/rocq#21478 Co-authored-by: Xavier Leroy <xavier.leroy@college-de-france.fr>
1 parent 821abd5 commit 4f8f2b1

File tree

2 files changed

+5
-5
lines changed

2 files changed

+5
-5
lines changed

backend/Cminor.v

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -194,15 +194,15 @@ Definition env := PTree.t val.
194194

195195
Fixpoint set_params (vl: list val) (il: list ident) {struct il} : env :=
196196
match il, vl with
197-
| i1 :: is, v1 :: vs => PTree.set i1 v1 (set_params vs is)
198-
| i1 :: is, nil => PTree.set i1 Vundef (set_params nil is)
197+
| i1 :: il, v1 :: vl => PTree.set i1 v1 (set_params vl il)
198+
| i1 :: il, nil => PTree.set i1 Vundef (set_params nil il)
199199
| _, _ => PTree.empty val
200200
end.
201201

202202
Fixpoint set_locals (il: list ident) (e: env) {struct il} : env :=
203203
match il with
204204
| nil => e
205-
| i1 :: is => PTree.set i1 Vundef (set_locals is e)
205+
| i1 :: il => PTree.set i1 Vundef (set_locals il e)
206206
end.
207207

208208
Definition set_optvar (optid: option ident) (v: val) (e: env) : env :=

cfrontend/Cminorgenproof.v

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1103,8 +1103,8 @@ Qed.
11031103

11041104
Fixpoint set_params' (vl: list val) (il: list ident) (te: Cminor.env) : Cminor.env :=
11051105
match il, vl with
1106-
| i1 :: is, v1 :: vs => set_params' vs is (PTree.set i1 v1 te)
1107-
| i1 :: is, nil => set_params' nil is (PTree.set i1 Vundef te)
1106+
| i1 :: il, v1 :: vl => set_params' vl il (PTree.set i1 v1 te)
1107+
| i1 :: il, nil => set_params' nil il (PTree.set i1 Vundef te)
11081108
| _, _ => te
11091109
end.
11101110

0 commit comments

Comments
 (0)