From 16061426080400749ca96fb140dd42042e51b7b9 Mon Sep 17 00:00:00 2001
From: Johannes Kloos <jkloos@mpi-sws.org>
Date: Tue, 24 Oct 2017 01:04:31 +0200
Subject: Fix part of 'Hard to find documentation for `(...) and `{...} #5631'

As discussed in the bug report, this adds `(...) and `{...} to the
index.
---
 doc/refman/RefMan-ext.tex | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b27a4dc94..5c519e46e 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1840,6 +1840,9 @@ This is useful for declaring the implicit type of a single variable.
 \subsection{Implicit generalization
 \label{implicit-generalization}
 \comindex{Generalizable Variables}}
+% \textquoteleft since \` doesn't do what we want
+\index{0genimpl@{\textquoteleft\{\ldots\}}}
+\index{0genexpl@{\textquoteleft(\ldots)}}
 
 Implicit generalization is an automatic elaboration of a statement with
 free variables into a closed statement where these variables are
-- 
cgit v1.2.3