From 31f0ec055d0cc3af9295b126d5a93cbc9538a5af Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 23 Feb 2016 14:32:38 +0100
Subject: [PATCH] Turn stuff like iRes Definitions instead of Notations.

With Set Printing All, these notations make me loose overview entirely.
---
 program_logic/model.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/program_logic/model.v b/program_logic/model.v
index 711b5bac8..6d4a5d147 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -31,11 +31,11 @@ End iProp.
 
 (* Solution *)
 Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
-Notation iRes Λ Σ := (res Λ Σ (laterC (iPreProp Λ Σ))).
-Notation iResRA Λ Σ := (resRA Λ Σ (laterC (iPreProp Λ Σ))).
-Notation iWld Λ Σ := (mapRA positive (agreeRA (laterC (iPreProp Λ Σ)))).
-Notation iPst Λ := (exclRA (istateC Λ)).
-Notation iGst Λ Σ := (ifunctor_car Σ (laterC (iPreProp Λ Σ))).
+Definition iRes Λ Σ := res Λ Σ (laterC (iPreProp Λ Σ)).
+Definition iResRA Λ Σ := resRA Λ Σ (laterC (iPreProp Λ Σ)).
+Definition iWld Λ Σ := mapRA positive (agreeRA (laterC (iPreProp Λ Σ))).
+Definition iPst Λ := exclRA (istateC Λ).
+Definition iGst Λ Σ := ifunctor_car Σ (laterC (iPreProp Λ Σ)).
 Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResRA Λ Σ).
 Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold _.
 Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.
-- 
GitLab