From 3e4dd12089a95c6420c3800e82c80a6a6608dc8c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 11:12:18 +0200
Subject: [PATCH] Comment about `diag_None`.

---
 theories/fin_maps.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index ff87fd5c..ea77ec1a 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -30,6 +30,11 @@ Class FinMapToList K A M := map_to_list: M → list (K * A).
 Global Hint Mode FinMapToList ! - - : typeclass_instances.
 Global Hint Mode FinMapToList - - ! : typeclass_instances.
 
+(** The function [diag_None f] is used in the specification and lemmas of
+[merge f]. It lifts a function [f : option A → option B → option C] by returning
+[None] if both arguments are [None], to make sure that in [merge f m1 m2], the
+function [f] can only operate on elements that are in the domain of either [m1]
+or [m2]. *)
 Definition diag_None {A B C} (f : option A → option B → option C)
     (mx : option A) (my : option B) : option C :=
   match mx, my with None, None => None | _, _ => f mx my end.
-- 
GitLab