From 7d8a8a775dee55eebe72d3146b054960c5c76b1d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 8 Jan 2026 08:41:37 +0100 Subject: [PATCH 1/2] Adapt to https://github.com/rocq-prover/rocq/pull/21478 --- backend/Cminor.v | 6 +++--- cfrontend/Cminorgenproof.v | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/backend/Cminor.v b/backend/Cminor.v index 1ba041fa2c..f9e83149cb 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 :: si, v1 :: vs => PTree.set i1 v1 (set_params vs si) + | i1 :: si, nil => PTree.set i1 Vundef (set_params nil si) | _, _ => 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 :: si => PTree.set i1 Vundef (set_locals si e) end. Definition set_optvar (optid: option ident) (v: val) (e: env) : env := diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 9fc50228e0..2a439f7cdd 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 :: si, v1 :: vs => set_params' vs si (PTree.set i1 v1 te) + | i1 :: si, nil => set_params' nil si (PTree.set i1 Vundef te) | _, _ => te end. From ed6ce4b724b02fe3740fee7edc344cc8b0c15388 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 27 Jan 2026 16:43:05 +0100 Subject: [PATCH 2/2] Use different, more consistent variable names --- backend/Cminor.v | 6 +++--- cfrontend/Cminorgenproof.v | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/backend/Cminor.v b/backend/Cminor.v index f9e83149cb..6cd61da3cc 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 :: si, v1 :: vs => PTree.set i1 v1 (set_params vs si) - | i1 :: si, nil => PTree.set i1 Vundef (set_params nil si) + | 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 :: si => PTree.set i1 Vundef (set_locals si 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 2a439f7cdd..8f09febb77 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 :: si, v1 :: vs => set_params' vs si (PTree.set i1 v1 te) - | i1 :: si, nil => set_params' nil si (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.