From 6f24ed4baa4d61967a95bac834eab2c66f3b76fa Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 11 Sep 2024 00:34:05 +0200 Subject: [PATCH] Bump std++. --- coq-iris.opam | 2 +- iris/proofmode/ltac_tactics.v | 10 +++++----- iris/proofmode/tokens.v | 10 +++++----- iris_heap_lang/proofmode.v | 2 +- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/coq-iris.opam b/coq-iris.opam index 34fbd4a5e..2a6738e3e 100644 --- a/coq-iris.opam +++ b/coq-iris.opam @@ -28,7 +28,7 @@ tags: [ depends: [ "coq" { (>= "8.18" & < "8.20~") | (= "dev") } - "coq-stdpp" { (= "dev.2024-09-08.0.d37b5e70") | (= "dev") } + "coq-stdpp" { (= "dev.2024-09-10.3.a1a12e00") | (= "dev") } ] build: ["./make-package" "iris" "-j%{jobs}%"] diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v index 4db325d7c..1018168a7 100644 --- a/iris/proofmode/ltac_tactics.v +++ b/iris/proofmode/ltac_tactics.v @@ -1196,7 +1196,7 @@ Tactic Notation "iSplit" := Tactic Notation "iSplitL" constr(Hs) := iStartProof; - let Hs := words Hs in + let Hs := String.words Hs in let Hs := eval vm_compute in (INamed <$> Hs) in let Δ := iGetCtx in eapply tac_sep_split with Left Hs _ _; (* (js:=Hs) *) @@ -1212,7 +1212,7 @@ Tactic Notation "iSplitL" constr(Hs) := Tactic Notation "iSplitR" constr(Hs) := iStartProof; - let Hs := words Hs in + let Hs := String.words Hs in let Hs := eval vm_compute in (INamed <$> Hs) in let Δ := iGetCtx in eapply tac_sep_split with Right Hs _ _; (* (js:=Hs) *) @@ -1481,7 +1481,7 @@ Tactic Notation "iDestructHyp" constr(H) "as" (** * Combinining hypotheses *) Tactic Notation "iCombine" constr(Hs) "as" constr(pat) := - let Hs := words Hs in + let Hs := String.words Hs in let Hs := eval vm_compute in (INamed <$> Hs) in let H := iFresh in let Δ := iGetCtx in @@ -1502,7 +1502,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) "as" constr(pat) := iCombine [H1;H2] as pat. Tactic Notation "iCombineGivesCore" constr(Hs) "gives" tactic3(tac) := - let Hs := words Hs in + let Hs := String.words Hs in let Hs := eval vm_compute in (INamed <$> Hs) in let H := iFresh in let Δ := iGetCtx in @@ -1534,7 +1534,7 @@ Tactic Notation "iCombine" constr(H1) constr(H2) Tactic Notation "iCombineAsGivesCore" constr(Hs) "as" constr(pat1) "gives" tactic3(tac) := - let Hs := words Hs in + let Hs := String.words Hs in let Hs := eval vm_compute in (INamed <$> Hs) in let H1 := iFresh in let H2 := iFresh in diff --git a/iris/proofmode/tokens.v b/iris/proofmode/tokens.v index a450d6c2f..8885c26d9 100644 --- a/iris/proofmode/tokens.v +++ b/iris/proofmode/tokens.v @@ -37,8 +37,8 @@ Inductive state := Definition cons_state (kn : state) (k : list token) : list token := match kn with | SNone => k - | SName s => TName (string_rev s) :: k - | SPure s => TPure (if String.eqb s "" then None else Some (string_rev s)) :: k + | SName s => TName (String.rev s) :: k + | SPure s => TPure (if String.eqb s "" then None else Some (String.rev s)) :: k | SNat n => TNat n :: k end. @@ -77,17 +77,17 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token := | String a s => (* TODO: Complain about invalid characters, to future-proof this against making more characters special. *) - if is_space a then tokenize_go s (cons_state kn k) SNone else + if Ascii.is_space a then tokenize_go s (cons_state kn k) SNone else match kn with | SNone => - match is_nat a with + match Ascii.is_nat a with | Some n => tokenize_go s k (SNat n) | None => tokenize_go s k (SName (String a "")) end | SName s' => tokenize_go s k (SName (String a s')) | SPure s' => tokenize_go s k (SPure (String a s')) | SNat n => - match is_nat a with + match Ascii.is_nat a with | Some n' => tokenize_go s k (SNat (n' + 10 * n)) | None => tokenize_go s (TNat n :: k) (SName (String a "")) end diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v index 1f33c430b..5fd51ed37 100644 --- a/iris_heap_lang/proofmode.v +++ b/iris_heap_lang/proofmode.v @@ -737,7 +737,7 @@ Tactic Notation "awp_apply" open_constr(lem) := last iAuIntro. Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) := (* Convert "list of hypothesis" into specialization pattern. *) - let Hs := words Hs in + let Hs := String.words Hs in let Hs := eval vm_compute in (INamed <$> Hs) in wp_apply_core lem ltac:(fun H => -- GitLab