From 53fe9f4028ceeb7346a528ad0748fd0f3de3edd5 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 4 Jan 2017 01:01:20 +0100
Subject: [PATCH] Correct stupid bug about interpretation scopes.

---
 theories/algebra/agree.v          | 4 +++-
 theories/program_logic/language.v | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 6353644d8..4e315737f 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 9c87c1e94..3227a06e1 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 {_} _ _ _ _ _.
-- 
GitLab