From 2ed3de6b8d13072e7f44ffca8f8aa7c6d6561c58 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Nov 2017 10:11:11 +0100
Subject: [PATCH] Fix some comments.

---
 theories/algebra/cmra.v | 2 +-
 theories/algebra/ofe.v  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 381e2e9fe..d35386930 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -1464,7 +1464,7 @@ Proof.
   by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
 Qed.
 
-(* Dependently-typed functions *)
+(* Dependently-typed functions over a finite domain *)
 Section ofe_fun_cmra.
   Context `{Hfin : Finite A} {B : A → ucmraT}.
   Implicit Types f g : ofe_fun B.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index c5e8e4042..eb422ac9b 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1087,7 +1087,7 @@ Proof.
   destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
 Qed.
 
-(* Dependently-typed functions *)
+(* Dependently-typed functions over a discrete domain *)
 (* We make [ofe_fun] a definition so that we can register it as a canonical
 structure. *)
 Definition ofe_fun {A} (B : A → ofeT) := ∀ x : A, B x.
-- 
GitLab