aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-05 18:20:36 +0200
committerHugo Herbelin2020-04-21 19:29:57 +0200
commitab14dab1f8a612e3d854df89ae6d21c26ebb2945 (patch)
tree24942a0d27ea149f3830c0bef23a78d8c67decf4
parent6908a9da72bc534d53493816d9b552c85d447f49 (diff)
Fixing #3451: coqdoc links for projections of tuples rather than for constructor.
Moreover, the link to the constructor was hiding other contents of the tuple.
Diffstat
-rw-r--r--interp/constrintern.ml2
-rw-r--r--test-suite/coqdoc/Record.html.out34
-rw-r--r--test-suite/coqdoc/Record.tex.out27
-rw-r--r--test-suite/coqdoc/Record.v2
-rw-r--r--test-suite/coqdoc/bug11194.html.out2
-rw-r--r--test-suite/coqdoc/bug11194.tex.out2
6 files changed, 67 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4bd0013750..f82783f47d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1432,6 +1432,7 @@ let sort_fields ~complete loc fields completer =
let (first_field_glob_ref, record) =
try
let gr = locate_reference first_field_ref in
+ Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr;
(gr, Recordops.find_projection gr)
with Not_found ->
raise (InternalizationError(first_field_ref.CAst.loc, NotAProjection first_field_ref))
@@ -1479,6 +1480,7 @@ let sort_fields ~complete loc fields completer =
by a let-in in the record declaration
(its value is fixed from other fields). *)
user_err ?loc (str "No local fields allowed in a record construction.");
+ Dumpglob.add_glob ?loc:field_ref.CAst.loc field_glob_ref;
index_fields fields remaining_projs ((field_index, field_value) :: acc)
| [] ->
let remaining_fields =
diff --git a/test-suite/coqdoc/Record.html.out b/test-suite/coqdoc/Record.html.out
new file mode 100644
index 0000000000..371188dfbe
--- /dev/null
+++ b/test-suite/coqdoc/Record.html.out
@@ -0,0 +1,34 @@
+<!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.Record</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library Coqdoc.Record</h1>
+
+<div class="code">
+<span class="id" title="keyword">Record</span> <a id="a" class="idref" href="#a"><span class="id" title="record">a</span></a> := { <a id="b" class="idref" href="#b"><span class="id" title="projection">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> ; <a id="c" class="idref" href="#c"><span class="id" title="projection">c</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> }.<br/>
+<span class="id" title="keyword">Definition</span> <a id="d" class="idref" href="#d"><span class="id" title="definition">d</span></a> := {| <a class="idref" href="Coqdoc.Record.html#b"><span class="id" title="projection">b</span></a> := 0 ; <a class="idref" href="Coqdoc.Record.html#c"><span class="id" title="projection">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</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/Record.tex.out b/test-suite/coqdoc/Record.tex.out
new file mode 100644
index 0000000000..4130ea9472
--- /dev/null
+++ b/test-suite/coqdoc/Record.tex.out
@@ -0,0 +1,27 @@
+\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.Record}{Library }{Coqdoc.Record}
+
+\begin{coqdoccode}
+\coqdocnoindent
+\coqdockw{Record} \coqdef{Coqdoc.Record.a}{a}{\coqdocrecord{a}} := \{ \coqdef{Coqdoc.Record.b}{b}{\coqdocprojection{b}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} ; \coqdef{Coqdoc.Record.c}{c}{\coqdocprojection{c}} : \coqexternalref{bool}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{bool}} \}.\coqdoceol
+\coqdocnoindent
+\coqdockw{Definition} \coqdef{Coqdoc.Record.d}{d}{\coqdocdefinition{d}} := \{| \coqref{Coqdoc.Record.b}{\coqdocprojection{b}} := 0 ; \coqref{Coqdoc.Record.c}{\coqdocprojection{c}} := \coqexternalref{true}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{true}} |\}.\coqdoceol
+\end{coqdoccode}
+\end{document}
diff --git a/test-suite/coqdoc/Record.v b/test-suite/coqdoc/Record.v
new file mode 100644
index 0000000000..f362aade98
--- /dev/null
+++ b/test-suite/coqdoc/Record.v
@@ -0,0 +1,2 @@
+Record a := { b : nat ; c : bool }.
+Definition d := {| b := 0 ; c := true |}.
diff --git a/test-suite/coqdoc/bug11194.html.out b/test-suite/coqdoc/bug11194.html.out
index 6fc6533e59..56bf6eaaca 100644
--- a/test-suite/coqdoc/bug11194.html.out
+++ b/test-suite/coqdoc/bug11194.html.out
@@ -20,7 +20,7 @@
<div class="code">
<span class="id" title="keyword">Record</span> <a id="a_struct" class="idref" href="#a_struct"><span class="id" title="record">a_struct</span></a> := { <a id="anum" class="idref" href="#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 id="a_struct_0" class="idref" href="#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">Canonical</span> <span class="id" title="keyword">Structure</span> <a id="a_struct_0" class="idref" href="#a_struct_0"><span class="id" title="definition">a_struct_0</span></a> := {| <a class="idref" href="Coqdoc.bug11194.html#anum"><span class="id" title="projection">anum</span></a> := 0|}.<br/>
<span class="id" title="keyword">Definition</span> <a id="rename_a_s_0" class="idref" href="#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 id="some_nat" class="idref" href="#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 id="rename_some_nat" class="idref" href="#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/>
diff --git a/test-suite/coqdoc/bug11194.tex.out b/test-suite/coqdoc/bug11194.tex.out
index 243dc20e8f..a262b45fc8 100644
--- a/test-suite/coqdoc/bug11194.tex.out
+++ b/test-suite/coqdoc/bug11194.tex.out
@@ -22,7 +22,7 @@
\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
+\coqdockw{Canonical} \coqdockw{Structure} \coqdef{Coqdoc.bug11194.a struct 0}{a\_struct\_0}{\coqdocdefinition{a\_struct\_0}} := \{| \coqref{Coqdoc.bug11194.anum}{\coqdocprojection{anum}} := 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 15:01:15 +0000