Fixing encoding in coqdoc output tests.

The file links.v is using utf-8 characters so this is needed at least to test this file. For the other files, it is not completely without effect since it makes that symbols like => and forall are respectively displayed ⇒ and ∀. Maybe tests with iso-8859-1 or test without a charset option should be kept.
author: Hugo Herbelin <Hugo.Herbelin@inria.fr> 2017-11-07 14:30:10 +0100
committer: Hugo Herbelin <Hugo.Herbelin@inria.fr> 2017-11-13 23:33:41 +0100
commit: f5c995467f8342e84bd73ac6d6bbd3c3281b2b4e (patch)
tree: 8eb227295d49de0ec60a4c17c07d5447f99b71e6 /test-suite/coqdoc
parent: 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff)
6 files changed, 46 insertions, 16 deletions
diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out
index 06789c1c1..5c5a2dc29 100644
--- a/test-suite/coqdoc/bug5648.html.out
+++ b/test-suite/coqdoc/bug5648.html.out
@@ -2,7 +2,7 @@
 "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" />
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
 <link href="coqdoc.css" rel="stylesheet" type="text/css" />
 <title>Coqdoc.bug5648</title>
 </head>
@@ -31,14 +31,14 @@
 <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;| <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> ⇒ 0<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> ⇒ 1<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> ⇒ 2<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Goal"><span class="id" title="constructor">Goal</span></a> ⇒ 3<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#L"><span class="id" title="constructor">L</span></a> ⇒ 4<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Lemma"><span class="id" title="constructor">Lemma</span></a> ⇒ 5<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#P"><span class="id" title="constructor">P</span></a> ⇒ 6<br/>
+&nbsp;&nbsp;| <a class="idref" href="Coqdoc.bug5648.html#Proof"><span class="id" title="constructor">Proof</span></a> ⇒ 7<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
 </div>
 </div>
diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out
index b0b732eff..82f7da230 100644
--- a/test-suite/coqdoc/bug5648.tex.out
+++ b/test-suite/coqdoc/bug5648.tex.out
@@ -1,5 +1,15 @@
 \documentclass[12pt]{report}
-\usepackage[]{inputenc}
+\usepackage[utf8x]{inputenc}
+
+%Warning: tipa declares many non-standard macros used by utf8x to
+%interpret utf8 characters but extra packages might have to be added
+%such as "textgreek" for Greek letters not already in tipa
+%or "stmaryrd" for mathematical symbols.
+%Utf8 codes missing a LaTeX interpretation can be defined by using
+%\DeclareUnicodeCharacter{code}{interpretation}.
+%Use coqdoc's option -p to add new packages or declarations.
+\usepackage{tipa}
+
 \usepackage[T1]{fontenc}
 \usepackage{fullpage}
 \usepackage{coqdoc}
diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out
index 0e05660d6..b96fc6281 100644
--- a/test-suite/coqdoc/bug5700.html.out
+++ b/test-suite/coqdoc/bug5700.html.out
@@ -2,7 +2,7 @@
 "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" />
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
 <link href="coqdoc.css" rel="stylesheet" type="text/css" />
 <title>Coqdoc.bug5700</title>
 </head>
diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out
index 33990cb89..1a1af5dfd 100644
--- a/test-suite/coqdoc/bug5700.tex.out
+++ b/test-suite/coqdoc/bug5700.tex.out
@@ -1,5 +1,15 @@
 \documentclass[12pt]{report}
-\usepackage[]{inputenc}
+\usepackage[utf8x]{inputenc}
+
+%Warning: tipa declares many non-standard macros used by utf8x to
+%interpret utf8 characters but extra packages might have to be added
+%such as "textgreek" for Greek letters not already in tipa
+%or "stmaryrd" for mathematical symbols.
+%Utf8 codes missing a LaTeX interpretation can be defined by using
+%\DeclareUnicodeCharacter{code}{interpretation}.
+%Use coqdoc's option -p to add new packages or declarations.
+\usepackage{tipa}
+
 \usepackage[T1]{fontenc}
 \usepackage{fullpage}
 \usepackage{coqdoc}
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
index e2928f78d..70cbe5065 100644
--- a/test-suite/coqdoc/links.html.out
+++ b/test-suite/coqdoc/links.html.out
@@ -2,7 +2,7 @@
 "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" />
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
 <link href="coqdoc.css" rel="stylesheet" type="text/css" />
 <title>Coqdoc.links</title>
 </head>
@@ -57,7 +57,7 @@ Various checks for coqdoc
 <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/>
+<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</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/>
@@ -74,7 +74,7 @@ Various checks for coqdoc
 <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/>
+<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">→</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="inductive">eq</span></a> <a class="idref" href="Coqdoc.links.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.links.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/>
 
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index de3182d1a..7d93189ae 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -1,5 +1,15 @@
 \documentclass[12pt]{report}
-\usepackage[]{inputenc}
+\usepackage[utf8x]{inputenc}
+
+%Warning: tipa declares many non-standard macros used by utf8x to
+%interpret utf8 characters but extra packages might have to be added
+%such as "textgreek" for Greek letters not already in tipa
+%or "stmaryrd" for mathematical symbols.
+%Utf8 codes missing a LaTeX interpretation can be defined by using
+%\DeclareUnicodeCharacter{code}{interpretation}.
+%Use coqdoc's option -p to add new packages or declarations.
+\usepackage{tipa}
+
 \usepackage[T1]{fontenc}
 \usepackage{fullpage}
 \usepackage{coqdoc}
author	Hugo Herbelin <Hugo.Herbelin@inria.fr>	2017-11-07 14:30:10 +0100
committer	Hugo Herbelin <Hugo.Herbelin@inria.fr>	2017-11-13 23:33:41 +0100
commit	f5c995467f8342e84bd73ac6d6bbd3c3281b2b4e (patch)
tree	8eb227295d49de0ec60a4c17c07d5447f99b71e6 /test-suite/coqdoc
parent	0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff)