From d4ecb8269b695a972c3e873f08be497b9257d146 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 7 Jun 2017 17:41:53 +0200
Subject: Refactor documentation of records.

This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971
---
 doc/common/macros.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 5abdecfc18..b36827f5da 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -145,7 +145,7 @@
 
 \newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}}
 \newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}}
-
+\newcommand{\typecstrtype}{\zeroone{{\tt :}~{\type}}}
 
 \newcommand{\Fwterm}{\nterm{Fwterm}}
 \newcommand{\Index}{\nterm{index}}
-- 
cgit v1.2.3