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();                                      /**. .**/