From 149997b59c6711c551490c4e7601eaac59f5f675 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Aug 2017 19:51:45 +0200
Subject: A first step at refreshing and documenting the new feature.

---
 doc/refman/RefMan-lib.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/refman/RefMan-lib.tex')

diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index c8e8443026..89f5be8438 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -55,6 +55,7 @@ Figure~\ref{init-notations}.
 \hline
 Notation & Precedence & Associativity \\
 \hline
+\verb!_ -> _! & 99 & right \\
 \verb!_ <-> _! & 95 & no \\
 \verb!_ \/ _!  & 85 & right \\
 \verb!_ /\ _!  & 80 & right \\
-- 
cgit v1.2.3