From f11955d622abd326fa2c211430c57876f5b8d43a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Aug 2016 13:36:40 +0200
Subject: [PATCH] Fix typos in the documentation of program_logic/model.

---
 program_logic/model.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/program_logic/model.v b/program_logic/model.v
index 789c57a5b..fe3a35d9e 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -5,7 +5,7 @@ From iris.algebra Require cofe_solver.
 (** In this file we construct the type [iProp] of propositions of the Iris
 logic. This is done by solving the following recursive domain equation:
 
-  iProp ≈ uPred { i : gid  &  gname -fin-> (Σ i) iProp }
+  iProp ≈ uPred (∀ i : gid, gname -fin-> (Σ i) iProp)
 
 where:
 
@@ -44,7 +44,7 @@ Coercion gFunctors_lookup : gFunctors >-> Funclass.
 
 Definition gname := positive.
 
-(** The resources functor [iResF Σ A := { i : gid & gname -fin-> (Σ i) A }]. *)
+(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
 Definition iResF (Σ : gFunctors) : urFunctor :=
   iprodURF (λ i, gmapURF gname (Σ i)).
 
-- 
GitLab