diff --git a/backend/Cminor.v b/backend/Cminor.v
index 1ba041fa2..6cd61da3c 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -194,15 +194,15 @@ Definition env := PTree.t val.
 
 Fixpoint set_params (vl: list val) (il: list ident) {struct il} : env :=
   match il, vl with
-  | i1 :: is, v1 :: vs => PTree.set i1 v1 (set_params vs is)
-  | i1 :: is, nil => PTree.set i1 Vundef (set_params nil is)
+  | i1 :: il, v1 :: vl => PTree.set i1 v1 (set_params vl il)
+  | i1 :: il, nil => PTree.set i1 Vundef (set_params nil il)
   | _, _ => PTree.empty val
   end.
 
 Fixpoint set_locals (il: list ident) (e: env) {struct il} : env :=
   match il with
   | nil => e
-  | i1 :: is => PTree.set i1 Vundef (set_locals is e)
+  | i1 :: il => PTree.set i1 Vundef (set_locals il e)
   end.
 
 Definition set_optvar (optid: option ident) (v: val) (e: env) : env :=
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 9fc50228e..8f09febb7 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1103,8 +1103,8 @@ Qed.
 
 Fixpoint set_params' (vl: list val) (il: list ident) (te: Cminor.env) : Cminor.env :=
   match il, vl with
-  | i1 :: is, v1 :: vs => set_params' vs is (PTree.set i1 v1 te)
-  | i1 :: is, nil => set_params' nil is (PTree.set i1 Vundef te)
+  | i1 :: il, v1 :: vl => set_params' vl il (PTree.set i1 v1 te)
+  | i1 :: il, nil => set_params' nil il (PTree.set i1 Vundef te)
   | _, _ => te
   end.