From 6bf23306e4442a1824229e3e088ca2df9aacc3fe Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 9 Jan 2026 08:46:54 +0100 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21478 --- LiveVerif/src/LiveVerif/LiveParsing.v | 2 +- LiveVerif/src/LiveVerifExamples/tree_set.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/LiveVerif/src/LiveVerif/LiveParsing.v b/LiveVerif/src/LiveVerif/LiveParsing.v index 27900f500..40becaf71 100644 --- a/LiveVerif/src/LiveVerif/LiveParsing.v +++ b/LiveVerif/src/LiveVerif/LiveParsing.v @@ -290,7 +290,7 @@ Proof. intros. reflexivity. Succeed Qed. Abort. Goal True. pose */ /* hello, world! */ /* as s. - pose */ /* The way we implement C comments is a bit limited: + pose */ /* The way we implement C comments appears a bit limited: - We can't use full stops - Only a few special characters are supported, eg ?, $, # - We can't use parentheses diff --git a/LiveVerif/src/LiveVerifExamples/tree_set.v b/LiveVerif/src/LiveVerifExamples/tree_set.v index 9b2266d56..3cf32075d 100644 --- a/LiveVerif/src/LiveVerifExamples/tree_set.v +++ b/LiveVerif/src/LiveVerifExamples/tree_set.v @@ -356,7 +356,7 @@ Derive bst_add SuchThat (fun_correct! bst_add) As bst_add_ok. return 1; /**. .**/ } /**. .**/ else { /**. .**/ - /* key not found, so we zoomed into the tree until it is empty, and + /* key not found, so we zoomed into the tree until it becomes empty, and shrinked the function's postcondition and the context -- there's no more tree around, and we'll just retrun a singleton tree! */ /**. .**/ uintptr_t res = bst_alloc_node(); /**. .**/