From ab14dab1f8a612e3d854df89ae6d21c26ebb2945 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 5 Apr 2020 18:20:36 +0200 Subject: 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. --- interp/constrintern.ml | 2 ++ test-suite/coqdoc/Record.html.out | 34 ++++++++++++++++++++++++++++++++++ test-suite/coqdoc/Record.tex.out | 27 +++++++++++++++++++++++++++ test-suite/coqdoc/Record.v | 2 ++ test-suite/coqdoc/bug11194.html.out | 2 +- test-suite/coqdoc/bug11194.tex.out | 2 +- 6 files changed, 67 insertions(+), 2 deletions(-) create mode 100644 test-suite/coqdoc/Record.html.out create mode 100644 test-suite/coqdoc/Record.tex.out create mode 100644 test-suite/coqdoc/Record.v 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 @@ + + + + + +Coqdoc.Record + + + + +
+ + + +
+ +

Library Coqdoc.Record

+ +
+Record a := { b : nat ; c : bool }.
+Definition d := {| b := 0 ; c := true |}.
+
+
+ + + +
+ + + \ 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 @@
Record a_struct := { anum : nat }.
-Canonical Structure a_struct_0 := {| anum := 0|}.
+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/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 -- cgit v1.2.3