diff options
| author | Théo Zimmermann | 2017-06-07 17:41:53 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2017-06-16 10:27:18 +0200 |
| commit | d4ecb8269b695a972c3e873f08be497b9257d146 (patch) | |
| tree | 381663797fae23d0eed348066c089ee08fd1be5a /doc/common | |
| parent | ce1e1dba837ad6e2c79ff7e531b5e3adea3cd327 (diff) | |
Refactor documentation of records.
This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971
Diffstat (limited to 'doc/common')
| -rw-r--r-- | doc/common/macros.tex | 2 |
1 files changed, 1 insertions, 1 deletions
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}} |