aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorHugo Herbelin2020-11-05 16:17:37 +0100
committerHugo Herbelin2020-11-14 22:55:47 +0100
commit696df507b58800a7a6b52741fd4ed859aff7b1c3 (patch)
treedff6216d09ee018319c27ca15472098f0502e039 /test-suite
parent0b12bb8c03b0ac7cc8aa7578a8db8ca93ecd1fd0 (diff)
Coqdoc: we move a newline at a better place.
This does not affect the rendering but gives better structured html/tex files.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/coqdoc/binder.tex.out3
-rw-r--r--test-suite/coqdoc/bug12742.tex.out1
-rw-r--r--test-suite/coqdoc/bug5700.tex.out6
-rw-r--r--test-suite/coqdoc/links.tex.out4
4 files changed, 10 insertions, 4 deletions
diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out
index 2b5648aee6..aceccc25fd 100644
--- a/test-suite/coqdoc/binder.tex.out
+++ b/test-suite/coqdoc/binder.tex.out
@@ -20,7 +20,8 @@
\begin{coqdoccode}
\end{coqdoccode}
-Link binders \begin{coqdoccode}
+Link binders
+\begin{coqdoccode}
\coqdocemptyline
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.binder.foo}{foo}{\coqdocdefinition{foo}} \coqdef{Coqdoc.binder.alpha:1}{alpha}{\coqdocbinder{alpha}} \coqdef{Coqdoc.binder.beta:2}{beta}{\coqdocbinder{beta}} := \coqref{Coqdoc.binder.alpha:1}{\coqdocvariable{alpha}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.binder.beta:2}{\coqdocvariable{beta}}.\coqdoceol
diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out
index d7eba096fc..a8f4c254cb 100644
--- a/test-suite/coqdoc/bug12742.tex.out
+++ b/test-suite/coqdoc/bug12742.tex.out
@@ -46,6 +46,7 @@ Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx
xxxxx xxxx xxxxxx.
\end{itemize}
+
\begin{coqdoccode}
\end{coqdoccode}
\end{document}
diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out
index 9dddb00450..f2b12f0079 100644
--- a/test-suite/coqdoc/bug5700.tex.out
+++ b/test-suite/coqdoc/bug5700.tex.out
@@ -20,12 +20,14 @@
\begin{coqdoccode}
\end{coqdoccode}
-\texttt{ foo (* \{bar\_bar\} *) } \begin{coqdoccode}
+\texttt{ foo (* \{bar\_bar\} *) }
+\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
-\texttt{ more (* nested (* comments *) within verbatim *) } \begin{coqdoccode}
+\texttt{ more (* nested (* comments *) within verbatim *) }
+\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol
\end{coqdoccode}
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index 2304f5ecc1..412a9ca6ac 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -36,6 +36,7 @@ Various checks for coqdoc
\item ``..'' should be rendered correctly
\end{itemize}
+
\begin{coqdoccode}
\coqdocemptyline
\coqdocnoindent
@@ -166,7 +167,8 @@ skip
skip
- skip \begin{coqdoccode}
+ skip
+\begin{coqdoccode}
\coqdocemptyline
\end{coqdoccode}
\end{document}