From 2744cd1871fce7e32f96fce58b83216e5612a92a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 25 May 2016 16:02:42 +0200
Subject: [PATCH] =?UTF-8?q?Turn=20some=20->=20arrows=20into=20=E2=86=92.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/base.v b/theories/base.v
index ab142229..7089551e 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -91,8 +91,8 @@ Notation "(, y )" := (λ x, (x,y)) (only parsing) : C_scope.
 Notation "p .1" := (fst p) (at level 10, format "p .1").
 Notation "p .2" := (snd p) (at level 10, format "p .2").
 
-Definition fun_map {A A' B B'} (f : A' -> A) (g : B -> B')
-  (h : A -> B) : A' -> B' := g ∘ h ∘ f.
+Definition fun_map {A A' B B'} (f : A' → A) (g : B → B')
+  (h : A → B) : A' → B' := g ∘ h ∘ f.
 Definition prod_map {A A' B B'} (f : A → A') (g : B → B')
   (p : A * B) : A' * B' := (f (p.1), g (p.2)).
 Arguments prod_map {_ _ _ _} _ _ !_ /.
-- 
GitLab