aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-16 09:37:21 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-08-16 09:37:21 +0200
commitf052c7fea6b0b9c0628ad77908ede7aac8712bd5 (patch)
tree98eed89cf4d4b78806e774716da53ebc1dbbb237
parentf0b4757d291ce3e07c8ccfcd4217d204fd2059ba (diff)
parentf3bb625fb2d118168042b97162e1ece1bda4a039 (diff)
Merge PR #880: Fix coqdoc bug #5648 on user idents colliding with keywords wrongly tagged as keywords
-rw-r--r--.gitignore2
-rw-r--r--test-suite/Makefile35
-rw-r--r--test-suite/coqdoc/bug5648.html.out53
-rw-r--r--test-suite/coqdoc/bug5648.tex.out49
-rw-r--r--test-suite/coqdoc/bug5648.v19
-rw-r--r--test-suite/coqdoc/links.html.out206
-rw-r--r--test-suite/coqdoc/links.tex.out162
-rw-r--r--tools/coqdoc/output.ml34
8 files changed, 540 insertions, 20 deletions
diff --git a/.gitignore b/.gitignore
index 71de7bb8d..5ee2f3f77 100644
--- a/.gitignore
+++ b/.gitignore
@@ -84,6 +84,8 @@ test-suite/coq-makefile/*/subdir/done
test-suite/coq-makefile/merlin1/.merlin
test-suite/coq-makefile/plugin-reach-outside-API-and-fail/_CoqProject
test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/_CoqProject
+test-suite/coqdoc/Coqdoc.*
+test-suite/coqdoc/index.html
# documentation
diff --git a/test-suite/Makefile b/test-suite/Makefile
index beb80a3df..1268ed14b 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -33,6 +33,7 @@ BIN := $(shell cd ..; pwd)/bin/
coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite
+coqdoc := $(BIN)coqdoc
coqtopbyte := $(BIN)coqtop.byte
coqtopload := $(coqtop) -top Top -async-proofs-cache force -load-vernac-source
@@ -85,7 +86,8 @@ COMPLEXITY := $(if $(bogomips),complexity)
BUGS := bugs/opened bugs/closed
VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
- output-modulo-time interactive micromega $(COMPLEXITY) modules stm
+ output-modulo-time interactive micromega $(COMPLEXITY) modules stm \
+ coqdoc
# All subsystems
SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coq-makefile
@@ -153,6 +155,7 @@ summary:
$(call summary_dir, "VI tests", vio); \
$(call summary_dir, "Coqchk tests", coqchk); \
$(call summary_dir, "Coq makefile", coq-makefile); \
+ $(call summary_dir, "Coqdoc tests", coqdoc); \
nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
nb_tests=`expr $$nb_success + $$nb_failure`; \
@@ -456,6 +459,8 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake))
fi; \
} > "$@"
+# vio compilation
+
vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
%.vio.log:%.v
@@ -473,6 +478,8 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v))
fi; \
} > "$@"
+# coqchk
+
coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
%.chk.log:%.v
@@ -489,6 +496,8 @@ coqchk: $(patsubst %.v,%.chk.log,$(wildcard coqchk/*.v))
fi; \
} > "$@"
+# coq_makefile
+
coq-makefile: $(patsubst %/run.sh,%.log,$(wildcard coq-makefile/*/run.sh))
coq-makefile/%.log : coq-makefile/%/run.sh
@@ -505,3 +514,27 @@ coq-makefile/%.log : coq-makefile/%/run.sh
echo " $<...Error!"; \
fi; \
) > "$@"
+
+# coqdoc
+
+coqdoc: $(patsubst %.sh,%.log,$(wildcard coqdoc/*.sh))
+
+$(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PREREQUISITELOG)
+ @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")"
+ $(HIDE){ \
+ echo $(call log_intro,$<); \
+ $(coqc) -R coqdoc Coqdoc $* 2>&1; \
+ cd coqdoc; \
+ f=`basename $*`; \
+ $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --html $$f.v; \
+ $(coqdoc) -R . Coqdoc -coqlib http://coq.inria.fr/stdlib --latex $$f.v; \
+ diff -u $$f.html.out Coqdoc.$$f.html 2>&1; R=$$?; times; \
+ grep -v "^%%" Coqdoc.$$f.tex | diff -u $$f.tex.out - 2>&1; S=$$?; times; \
+ if [ $$R = 0 -a $$S = 0 ]; then \
+ echo $(log_success); \
+ echo " $<...Ok"; \
+ else \
+ echo $(log_failure); \
+ echo " $<...Error! (unexpected output)"; \
+ fi; \
+ } > "$@"
diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out
new file mode 100644
index 000000000..06789c1c1
--- /dev/null
+++ b/test-suite/coqdoc/bug5648.html.out
@@ -0,0 +1,53 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>Coqdoc.bug5648</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.bug5648</h1>
+
+<div class="code">
+<span class="id" title="keyword">Lemma</span> <a name="a"><span class="id" title="lemma">a</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/>
+<span class="id" title="keyword">Proof</span>.<br/>
+<span class="id" title="tactic">auto</span>.<br/>
+<span class="id" title="keyword">Qed</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variant</span> <a name="t"><span class="id" title="inductive">t</span></a> :=<br/>
+| <a name="A"><span class="id" title="constructor">A</span></a> | <a name="Add"><span class="id" title="constructor">Add</span></a> | <a name="G"><span class="id" title="constructor">G</span></a> | <a name="Goal"><span class="id" title="constructor">Goal</span></a> | <a name="L"><span class="id" title="constructor">L</span></a> | <a name="Lemma"><span class="id" title="constructor">Lemma</span></a> | <a name="P"><span class="id" title="constructor">P</span></a> | <a name="Proof"><span class="id" title="constructor">Proof</span></a> .<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> <span class="id" title="var">x</span> :=<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> =&gt; 0<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> =&gt; 1<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> =&gt; 2<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Goal"><span class="id" title="constructor">Goal</span></a> =&gt; 3<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#L"><span class="id" title="constructor">L</span></a> =&gt; 4<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Lemma"><span class="id" title="constructor">Lemma</span></a> =&gt; 5<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> =&gt; 6<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> =&gt; 7<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html> \ No newline at end of file
diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out
new file mode 100644
index 000000000..b0b732eff
--- /dev/null
+++ b/test-suite/coqdoc/bug5648.tex.out
@@ -0,0 +1,49 @@
+\documentclass[12pt]{report}
+\usepackage[]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+\usepackage{amsmath,amssymb}
+\usepackage{url}
+\begin{document}
+\coqlibrary{Coqdoc.bug5648}{Library }{Coqdoc.bug5648}
+
+\begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Lemma} \coqdef{Coqdoc.bug5648.a}{a}{\coqdoclemma{a}} : \coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}.\coqdoceol
+\coqdocnoindent
+\coqdockw{Proof}.\coqdoceol
+\coqdocnoindent
+\coqdoctac{auto}.\coqdoceol
+\coqdocnoindent
+\coqdockw{Qed}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Variant} \coqdef{Coqdoc.bug5648.t}{t}{\coqdocinductive{t}} :=\coqdoceol
+\coqdocnoindent
+\ensuremath{|} \coqdef{Coqdoc.bug5648.A}{A}{\coqdocconstructor{A}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Add}{Add}{\coqdocconstructor{Add}} \ensuremath{|} \coqdef{Coqdoc.bug5648.G}{G}{\coqdocconstructor{G}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Goal}{Goal}{\coqdocconstructor{Goal}} \ensuremath{|} \coqdef{Coqdoc.bug5648.L}{L}{\coqdocconstructor{L}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Lemma}{Lemma}{\coqdocconstructor{Lemma}} \ensuremath{|} \coqdef{Coqdoc.bug5648.P}{P}{\coqdocconstructor{P}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Proof}{Proof}{\coqdocconstructor{Proof}} .\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdocvar{x} :=\coqdoceol
+\coqdocindent{1.00em}
+\coqdockw{match} \coqdocvariable{x} \coqdockw{with}\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqref{Coqdoc.bug5648.A}{\coqdocconstructor{A}} \ensuremath{\Rightarrow} 0\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqref{Coqdoc.bug5648.Add}{\coqdocconstructor{Add}} \ensuremath{\Rightarrow} 1\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqref{Coqdoc.bug5648.G}{\coqdocconstructor{G}} \ensuremath{\Rightarrow} 2\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqref{Coqdoc.bug5648.Goal}{\coqdocconstructor{Goal}} \ensuremath{\Rightarrow} 3\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqref{Coqdoc.bug5648.L}{\coqdocconstructor{L}} \ensuremath{\Rightarrow} 4\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqref{Coqdoc.bug5648.Lemma}{\coqdocconstructor{Lemma}} \ensuremath{\Rightarrow} 5\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqref{Coqdoc.bug5648.P}{\coqdocconstructor{P}} \ensuremath{\Rightarrow} 6\coqdoceol
+\coqdocindent{1.00em}
+\ensuremath{|} \coqref{Coqdoc.bug5648.Proof}{\coqdocconstructor{Proof}} \ensuremath{\Rightarrow} 7\coqdoceol
+\coqdocindent{1.00em}
+\coqdockw{end}.\coqdoceol
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/bug5648.v b/test-suite/coqdoc/bug5648.v
new file mode 100644
index 000000000..9b62dd1e1
--- /dev/null
+++ b/test-suite/coqdoc/bug5648.v
@@ -0,0 +1,19 @@
+Lemma a : True.
+Proof.
+auto.
+Qed.
+
+Variant t :=
+| A | Add | G | Goal | L | Lemma | P | Proof .
+
+Definition d x :=
+ match x with
+ | A => 0
+ | Add => 1
+ | G => 2
+ | Goal => 3
+ | L => 4
+ | Lemma => 5
+ | P => 6
+ | Proof => 7
+ end.
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
new file mode 100644
index 000000000..7d7d01c1b
--- /dev/null
+++ b/test-suite/coqdoc/links.html.out
@@ -0,0 +1,206 @@
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />
+<link href="coqdoc.css" rel="stylesheet" type="text/css" />
+<title>Coqdoc.links</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.links</h1>
+
+<div class="code">
+</div>
+
+<div class="doc">
+Various checks for coqdoc
+
+<div class="paragraph"> </div>
+
+<ul class="doclist">
+<li> symbols should not be inlined in string g
+
+</li>
+<li> links to both kinds of notations in a' should work to the right notation
+
+</li>
+<li> with utf8 option, forall must be unicode
+
+</li>
+<li> splitting between symbols and ident should be correct in a' and c
+
+</li>
+<li> ".." should be rendered correctly
+
+</li>
+</ul>
+
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Strings.String.html#"><span class="id" title="library">String</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="g"><span class="id" title="definition">g</span></a> := "dfjkh""sdfhj forall &lt;&gt; * ~"%<span class="id" title="var">string</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> (<span class="id" title="var">b</span>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) := <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">forall</span> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><span class="id" title="variable">C</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">&quot;</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">&quot;</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">&quot;</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">&quot;</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">&quot;</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/>
+
+<br/>
+<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a><a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a><br/>
+<br/>
+<span class="id" title="keyword">where</span> <a name="8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">&quot;</span></a>x = y :&gt; A" := (@<a class="idref" href="Coqdoc.links.html#eq"><span class="id" title="variable">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">&quot;</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#548d1059c499c9b2a9b95b07e68c2090"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#6b97e27793a3d22f5c0d1dd63170fd68"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">))</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Notation</span> <a name="h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Section</span> <a name="test"><span class="id" title="section">test</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Variables</span> <a name="test.b'"><span class="id" title="variable">b'</span></a> <a name="test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a name="4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">&quot;</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#3e01fbae4590c7b7699ff99ce61580e1"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">my_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">my</span>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a name="l"><span class="id" title="abbreviation">l</span></a> := 0.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#4ab0449b36c75cf94e08c5822ea83e3d"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#5bf2050e90b21ebc82dc5463d1ba338e"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#3dcaec3b772747610227247939f96b01"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">Admitted</span>.<br/>
+
+<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test"><span class="id" title="section">test</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">Section</span> <a name="test2"><span class="id" title="section">test2</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Variables</span> <a name="test2.b'"><span class="id" title="variable">b'</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Section</span> <a name="test2.test"><span class="id" title="section">test</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Variables</span> <a name="test2.test.b2"><span class="id" title="variable">b2</span></a>: <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <span class="id" title="var">b</span> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#1a1c7f13320341c3638e9edcc3e6389d"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#347f39a83bf7d45676cff54fd7e8966f"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/>
+
+<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2.test"><span class="id" title="section">test</span></a>.<br/>
+
+<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2"><span class="id" title="section">test2</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+<div class="paragraph"> </div>
+
+ skip
+</div>
+<div class="code">
+
+<br/>
+</div>
+</div>
+
+<div id="footer">
+<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
+</div>
+
+</div>
+
+</body>
+</html> \ No newline at end of file
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
new file mode 100644
index 000000000..844fb3031
--- /dev/null
+++ b/test-suite/coqdoc/links.tex.out
@@ -0,0 +1,162 @@
+\documentclass[12pt]{report}
+\usepackage[]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage{fullpage}
+\usepackage{coqdoc}
+\usepackage{amsmath,amssymb}
+\usepackage{url}
+\begin{document}
+\coqlibrary{Coqdoc.links}{Library }{Coqdoc.links}
+
+\begin{coqdoccode}
+\end{coqdoccode}
+Various checks for coqdoc
+
+
+
+\begin{itemize}
+\item symbols should not be inlined in string g
+
+\item links to both kinds of notations in a' should work to the right notation
+
+\item with utf8 option, forall must be unicode
+
+\item splitting between symbols and ident should be correct in a' and c
+
+\item ``..'' should be rendered correctly
+
+\end{itemize}
+\begin{coqdoccode}
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Require} \coqdockw{Import} \coqexternalref{}{http://coq.inria.fr/stdlib/Coq.Strings.String}{\coqdoclibrary{String}}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.links.g}{g}{\coqdocdefinition{g}} := "dfjkh""sdfhj forall <> * \~{}"\%\coqdocvar{string}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdocvar{b}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqdocvariable{b}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline
+\coqdocnoindent
+\coqdockw{Notation} \coqdef{Coqdoc.links.::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Notation} \coqdef{Coqdoc.links.::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Notation} \coqdef{Coqdoc.links.::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{:type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol
+\coqdocnoindent
+\coqdoceol
+\coqdocnoindent
+\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqdocvariable{eq} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Notation} \coqdef{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol
+\coqdocemptyline
+\coqdocnoindent
+\coqdockw{Notation} \coqdef{Coqdoc.links.h}{h}{\coqdocabbreviation{h}} := \coqref{Coqdoc.links.a}{\coqdocdefinition{a}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{1.00em}
+\coqdockw{Section} \coqdef{Coqdoc.links.test}{test}{\coqdocsection{test}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Variables} \coqdef{Coqdoc.links.test.b'}{b'}{\coqdocvariable{b'}} \coqdef{Coqdoc.links.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Notation} \coqdef{Coqdoc.links.test.:my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Delimit} \coqdockw{Scope} \coqdocvar{my\_scope} \coqdockw{with} \coqdocvar{my}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Notation} \coqdef{Coqdoc.links.l}{l}{\coqdocabbreviation{l}} := 0.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.:my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{:type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdocindent{2.00em}
+\coqdocvar{Admitted}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{1.00em}
+\coqdockw{End} \coqref{Coqdoc.links.test}{\coqdocsection{test}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{1.00em}
+\coqdockw{Section} \coqdef{Coqdoc.links.test2}{test2}{\coqdocsection{test2}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Variables} \coqdef{Coqdoc.links.test2.b'}{b'}{\coqdocvariable{b'}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{Section} \coqdef{Coqdoc.links.test2.test}{test}{\coqdocsection{test}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{3.00em}
+\coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{3.00em}
+\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol
+\coqdocemptyline
+\coqdocindent{2.00em}
+\coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol
+\coqdocemptyline
+\coqdocindent{1.00em}
+\coqdockw{End} \coqref{Coqdoc.links.test2}{\coqdocsection{test2}}.\coqdoceol
+\coqdocemptyline
+\end{coqdoccode}
+skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip
+
+ skip \begin{coqdoccode}
+\coqdocemptyline
+\end{coqdoccode}
+\end{document}
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 5c0d2a39b..d043c4a58 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -693,25 +693,21 @@ module Html = struct
printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
let ident s loc =
- if is_keyword s then begin
- printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
- end else begin
- try
- match loc with
- | None -> raise Not_found
- | Some loc ->
- reference (translate s) (Index.find (get_module false) loc)
- with Not_found ->
- if is_tactic s then
- printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
- else
- if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
- then
- try reference (translate s) (Index.find_string (get_module false) s)
- with _ -> Tokens.output_tagged_ident_string s
- else
- Tokens.output_tagged_ident_string s
- end
+ try
+ match loc with
+ | None -> raise Not_found
+ | Some loc ->
+ reference (translate s) (Index.find (get_module false) loc)
+ with Not_found ->
+ if is_tactic s then
+ printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
+ else if is_keyword s then
+ printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
+ else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then
+ try reference (translate s) (Index.find_string (get_module false) s)
+ with Not_found -> Tokens.output_tagged_ident_string s
+ else
+ Tokens.output_tagged_ident_string s
let proofbox () = printf "<font size=-2>&#9744;</font>"