Fixes #11194 (Canonical/Coercion not located for coqdoc).

The location was missing in the parser.
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
parent: c5c8ce135606f311834d4c0b9ac3e72be5ee4a36 (diff)
4 files changed, 78 insertions, 3 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.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 6de20c64a5..31fc54c1fa 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -694,17 +694,17 @@ GRAMMAR EXTEND Gram
       | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] ->
           { match ud with
            | None ->
-             VernacCanonical CAst.(make ~loc @@ AN qid)
+             VernacCanonical CAst.(make ?loc:qid.CAst.loc @@ AN qid)
            | Some (u,d) ->
              let s = coerce_reference_to_id qid in
-             VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) }
+             VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d) }
       | IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation ->
           { VernacCanonical CAst.(make ~loc @@ ByNotation ntn) }
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; u = OPT univ_decl; d = def_body ->
           { let s = coerce_reference_to_id qid in
-          VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),u),d) }
+          VernacDefinition ((NoDischarge,Coercion),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d) }
       | IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
          s = class_rawexpr; ">->"; t = class_rawexpr ->
            { VernacIdentityCoercion (f, s, t) }
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
parent	c5c8ce135606f311834d4c0b9ac3e72be5ee4a36 (diff)