diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 6353644d89fb0c5dc7a3575d302f67523046a985..4e315737f7f9033dfad3963ad79396f39ca161e7 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -22,7 +22,9 @@ Definition list_setincl `(R : relation A) (al bl : list A) :=
   ∀ a, a ∈ al → ∃ b, b ∈ bl ∧ R a b.
 Definition list_setequiv `(R : relation A) (al bl : list A) :=
   list_setincl R al bl ∧ list_setincl R bl al.
-(* list_agrees is carefully written such that, when applied to a singleton, it is convertible to True. This makes working with agreement much more pleasant. *)
+(* list_agrees is carefully written such that, when applied to a
+   singleton, it is convertible to True. This makes working with
+   agreement much more pleasant. *)
 Definition list_agrees `(R : relation A) (al : list A) :=
   match al with
   | [] => True
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 9c87c1e94ce3bf1f257c02d7247f619d993342d2..3227a06e1aa6f50b79740fa88c9ac318788f7cb8 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -15,7 +15,7 @@ Structure language := Language {
 Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.
 Bind Scope expr_scope with expr.
-Bind Scope expr_scope with val.
+Bind Scope val_scope with val.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
 Arguments prim_step {_} _ _ _ _ _.