From 52c1c25936deadffa7149a36b58a7342f902f259 Mon Sep 17 00:00:00 2001 From: Jan-Oliver Kaiser Date: Fri, 11 Sep 2026 12:31:29 +0200 Subject: [PATCH] Adapt to wp_path changes --- rocq-brick-libstdcpp/test/new/demo_cpp_proof.v | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v b/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v index de3b77b5..f7da9fba 100644 --- a/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/new/demo_cpp_proof.v @@ -53,11 +53,9 @@ Section with_cpp. Lemma test_delete_array_ok : verify[demo_cpp.source] "test_delete_array(int* )". Proof. verify_spec; go. - case_bool_decide; try by go. - go. - case_bool_decide. - { go. rewrite H. go. exfalso; lia. } - { go. } + case_bool_decide; go; []. + case_bool_decide as Hnull; go; []. + go. rewrite Hnull. go. exfalso; lia. Qed. (** The C++ standard recommends <<262144 <= SIZE_MAX>>. *)