From e9e55145d63b59995b1d5b4ba0843963ecb98b6c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 29 Aug 2016 19:23:15 +0200
Subject: [PATCH] Turn iProp into a notation.

This avoids Coq distinguishing iProp and uPred (iResUR _) when it
should not.
---
 program_logic/model.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/program_logic/model.v b/program_logic/model.v
index 212d2a740..f0199b825 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -116,7 +116,7 @@ Module Type iProp_solution_sig.
   Parameter iPreProp : gFunctors → cofeT.
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
-  Definition iProp (Σ : gFunctors) : cofeT := uPredC (iResUR Σ).
+  Notation iProp Σ := (uPredC (iResUR Σ)).
 
   Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
   Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ.
@@ -134,7 +134,7 @@ Module Export iProp_solution : iProp_solution_sig.
   Definition iPreProp (Σ : gFunctors) : cofeT := iProp_result Σ.
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
-  Definition iProp (Σ : gFunctors) : cofeT := uPredC (iResUR Σ).
+  Notation iProp Σ := (uPredC (iResUR Σ)).
 
   Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
     solution_fold (iProp_result Σ).
@@ -145,8 +145,6 @@ Module Export iProp_solution : iProp_solution_sig.
   Proof. apply solution_fold_unfold. Qed.
 End iProp_solution.
 
-Bind Scope uPred_scope with iProp.
-
 
 (** * Properties of the solution to the recursive domain equation *)
 Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
-- 
GitLab