From 23f7fac4e35360bd1241e501cda51307048daa89 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Feb 2016 16:29:51 +0100
Subject: [PATCH] bind types to scopes as early as possible, to functions get
 their arguments set appropriately

---
 algebra/upred.v       | 8 ++++----
 heap_lang/heap_lang.v | 3 +++
 heap_lang/notation.v  | 3 ---
 3 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 3aa4b20bf..c3279bd97 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -15,6 +15,10 @@ Local Transparent uPred_holds.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
 
+Delimit Scope uPred_scope with I.
+Bind Scope uPred_scope with uPred.
+Arguments uPred_holds {_} _%I _ _.
+
 Section cofe.
   Context {M : cmraT}.
   Instance uPred_equiv : Equiv (uPred M) := λ P Q, ∀ x n,
@@ -185,10 +189,6 @@ Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
   {| uPred_holds n x := ✓{n} a |}.
 Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
 
-Delimit Scope uPred_scope with I.
-Bind Scope uPred_scope with uPred.
-Arguments uPred_holds {_} _%I _ _.
-Arguments uPred_entails _ _%I _%I.
 Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
 Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
 Notation "■ φ" := (uPred_const φ%C%type)
diff --git a/heap_lang/heap_lang.v b/heap_lang/heap_lang.v
index eba609456..be2503d78 100644
--- a/heap_lang/heap_lang.v
+++ b/heap_lang/heap_lang.v
@@ -49,6 +49,9 @@ Inductive val :=
   | InjRV (v : val)
   | LocV (l : loc).
 
+Delimit Scope lang_scope with L.
+Bind Scope lang_scope with expr val.
+
 Fixpoint of_val (v : val) : expr :=
   match v with
   | RecV f x e => Rec f x e
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index fb7efc5da..fe4affa41 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -1,8 +1,5 @@
 Require Export heap_lang.derived.
 
-Delimit Scope lang_scope with L.
-Bind Scope lang_scope with expr val.
-
 (* What about Arguments for hoare triples?. *)
 Arguments wp {_ _} _ _%L _.
 
-- 
GitLab