From b07c136f1ef950ed16045d6a31af94c4782a56ab Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Fri, 13 Sep 2024 23:58:54 +0100
Subject: [PATCH] Fix proof breakage by not importing String module.
---
coq-diaframe.opam | 2 +-
diaframe/lib/own/validity_tactics.v | 2 +-
diaframe/steps/ipm_hyp_utils.v | 2 +-
3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/coq-diaframe.opam b/coq-diaframe.opam
index 00be89a3..f1403ae9 100644
--- a/coq-diaframe.opam
+++ b/coq-diaframe.opam
@@ -7,7 +7,7 @@ authors: "Ike Mulder <me@ikemulder.nl>"
homepage: "https://gitlab.mpi-sws.org/iris/diaframe/"
bug-reports: "https://gitlab.mpi-sws.org/iris/diaframe/-/issues"
depends: [
- "coq-iris" { (>= "dev.2024-08-16.3.8890e30a" & <= "dev.2024-09-10.0.f14ebfde" ) | = "dev" | = "4.1.0" }
+ "coq-iris" { (>= "dev.2024-08-16.3.8890e30a" & <= "dev.2024-09-11.3.0203d5ca" ) | = "dev" | = "4.1.0" }
"coq" { >= "8.18" & < "8.20~" }
]
build: [make "-j%{jobs}%" "diaframe"]
diff --git a/diaframe/lib/own/validity_tactics.v b/diaframe/lib/own/validity_tactics.v
index 8acbc48d..edfa1121 100644
--- a/diaframe/lib/own/validity_tactics.v
+++ b/diaframe/lib/own/validity_tactics.v
@@ -64,7 +64,7 @@ Proof.
Qed.
Ltac iCombineOwn_tac' Hs_raw destructstr :=
- let Hs := words Hs_raw in
+ let Hs := String.words Hs_raw in
let get_hyp_type Hname :=
let Δ := match goal with | |- environments.envs_entails ?Δ _ => Δ end in
let lookup := eval pm_eval in (environments.envs_lookup (INamed Hname) Δ) in
diff --git a/diaframe/steps/ipm_hyp_utils.v b/diaframe/steps/ipm_hyp_utils.v
index 052745f5..84b698fb 100644
--- a/diaframe/steps/ipm_hyp_utils.v
+++ b/diaframe/steps/ipm_hyp_utils.v
@@ -48,7 +48,7 @@ Ltac2 string_to_coq_string (s : string) : constr :=
let coq_byte_list : constr list
:= List.init (String.length s) (fun i => char_to_coq_byte (String.get s i)) in
let coq_bytes : constr := list_to_coq_list coq_byte_list in
- let raw_result : constr := '(string_of_list_byte $coq_bytes) in
+ let raw_result : constr := '(String.string_of_list_byte $coq_bytes) in
let result := Std.eval_cbv cbv_flags raw_result in
result.
--
GitLab