diff options
| author | Hugo Herbelin | 2020-04-05 15:22:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-05 15:43:04 +0200 |
| commit | 825f001fc03f94ee8076a33e34312f5d4a76eafb (patch) | |
| tree | 52492d5b4de6c5849c6729e6f19689097d394bbb /test-suite | |
| parent | c5c8ce135606f311834d4c0b9ac3e72be5ee4a36 (diff) | |
Fixes #11194 (Canonical/Coercion not located for coqdoc).
The location was missing in the parser.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/coqdoc/bug11194.html.out | 37 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug11194.tex.out | 33 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug11194.v | 5 |
3 files changed, 75 insertions, 0 deletions
diff --git a/test-suite/coqdoc/bug11194.html.out b/test-suite/coqdoc/bug11194.html.out new file mode 100644 index 0000000000..304d041033 --- /dev/null +++ b/test-suite/coqdoc/bug11194.html.out @@ -0,0 +1,37 @@ +<!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=utf-8" /> +<link href="coqdoc.css" rel="stylesheet" type="text/css" /> +<title>Coqdoc.bug11194</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug11194</h1> + +<div class="code"> +<span class="id" title="keyword">Record</span> <a name="a_struct"><span class="id" title="record">a_struct</span></a> := { <a name="anum"><span class="id" title="projection">anum</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/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="keyword">Structure</span> <a name="a_struct_0"><span class="id" title="definition">a_struct_0</span></a> := {| <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">anum</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">:=</span></a> <a class="idref" href="Coqdoc.bug11194.html#Build_a_struct"><span class="id" title="constructor">0</span></a>|}.<br/> +<span class="id" title="keyword">Definition</span> <a name="rename_a_s_0"><span class="id" title="definition">rename_a_s_0</span></a> := <a class="idref" href="Coqdoc.bug11194.html#a_struct_0"><span class="id" title="definition">a_struct_0</span></a>.<br/> +<span class="id" title="keyword">Coercion</span> <a name="some_nat"><span class="id" title="definition">some_nat</span></a> := (@<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</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/> +<span class="id" title="keyword">Definition</span> <a name="rename_some_nat"><span class="id" title="definition">rename_some_nat</span></a> := <a class="idref" href="Coqdoc.bug11194.html#some_nat"><span class="id" title="definition">some_nat</span></a>.<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/bug11194.tex.out b/test-suite/coqdoc/bug11194.tex.out new file mode 100644 index 0000000000..243dc20e8f --- /dev/null +++ b/test-suite/coqdoc/bug11194.tex.out @@ -0,0 +1,33 @@ +\documentclass[12pt]{report} +\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} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug11194}{Library }{Coqdoc.bug11194} + +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Record} \coqdef{Coqdoc.bug11194.a struct}{a\_struct}{\coqdocrecord{a\_struct}} := \{ \coqdef{Coqdoc.bug11194.anum}{anum}{\coqdocprojection{anum}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \}.\coqdoceol +\coqdocnoindent +\coqdockw{Canonical} \coqdockw{Structure} \coqdef{Coqdoc.bug11194.a struct 0}{a\_struct\_0}{\coqdocdefinition{a\_struct\_0}} := \{| \coqref{Coqdoc.bug11194.Build a struct}{\coqdocconstructor{anum}} \coqref{Coqdoc.bug11194.Build a struct}{\coqdocconstructor{:=}} \coqref{Coqdoc.bug11194.Build a struct}{\coqdocconstructor{0}}|\}.\coqdoceol +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug11194.rename a s 0}{rename\_a\_s\_0}{\coqdocdefinition{rename\_a\_s\_0}} := \coqref{Coqdoc.bug11194.a struct 0}{\coqdocdefinition{a\_struct\_0}}.\coqdoceol +\coqdocnoindent +\coqdockw{Coercion} \coqdef{Coqdoc.bug11194.some nat}{some\_nat}{\coqdocdefinition{some\_nat}} := (@\coqexternalref{Some}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{Some}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}).\coqdoceol +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug11194.rename some nat}{rename\_some\_nat}{\coqdocdefinition{rename\_some\_nat}} := \coqref{Coqdoc.bug11194.some nat}{\coqdocdefinition{some\_nat}}.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug11194.v b/test-suite/coqdoc/bug11194.v new file mode 100644 index 0000000000..b1d2a54f25 --- /dev/null +++ b/test-suite/coqdoc/bug11194.v @@ -0,0 +1,5 @@ +Record a_struct := { anum : nat }. +Canonical Structure a_struct_0 := {| anum := 0|}. +Definition rename_a_s_0 := a_struct_0. +Coercion some_nat := (@Some nat). +Definition rename_some_nat := some_nat. |