From ce233d5b4a6f8d506c37a2a492679a66f9618a94 Mon Sep 17 00:00:00 2001 From: Thomas Letan Date: Wed, 29 Jul 2020 14:53:19 +0200 Subject: coqdoc: Fix the “details” environment The change introduced by 41a1d66 has broken the feature prior to its initial release. We attempt to fix the issue, and add a comment to warn feature developers in order to avoid facing the same issue again. --- test-suite/coqdoc/details.html.out | 48 ++++++++++++++++++++++++++++++++++++++ test-suite/coqdoc/details.tex.out | 44 ++++++++++++++++++++++++++++++++++ test-suite/coqdoc/details.v | 11 +++++++++ 3 files changed, 103 insertions(+) create mode 100644 test-suite/coqdoc/details.html.out create mode 100644 test-suite/coqdoc/details.tex.out create mode 100644 test-suite/coqdoc/details.v (limited to 'test-suite') diff --git a/test-suite/coqdoc/details.html.out b/test-suite/coqdoc/details.html.out new file mode 100644 index 0000000000..e1f1ad9867 --- /dev/null +++ b/test-suite/coqdoc/details.html.out @@ -0,0 +1,48 @@ + + + + + +Coqdoc.details + + + + +
+ + + +
+ +

Library Coqdoc.details

+ +
+
+
+Definition foo : nat := 3.
+
+
+ +
+
+
Foo bar
+Fixpoint idnat (x : nat) : nat :=
+  match x with
+  | S x ⇒ S (idnat x)
+  | 0 ⇒ 0
+  end.
+
+
+
+
+ + + +
+ + + \ No newline at end of file diff --git a/test-suite/coqdoc/details.tex.out b/test-suite/coqdoc/details.tex.out new file mode 100644 index 0000000000..37778944ba --- /dev/null +++ b/test-suite/coqdoc/details.tex.out @@ -0,0 +1,44 @@ +\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.details}{Library }{Coqdoc.details} + +\begin{coqdoccode} +\end{coqdoccode} +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.details.foo}{foo}{\coqdocdefinition{foo}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} := 3.\coqdoceol +\end{coqdoccode} +\begin{coqdoccode} +\coqdocemptyline +\end{coqdoccode} +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Fixpoint} \coqdef{Coqdoc.details.idnat}{idnat}{\coqdocdefinition{idnat}} (\coqdef{Coqdoc.details.x:1}{x}{\coqdocbinder{x}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} :=\coqdoceol +\coqdocindent{1.00em} +\coqdockw{match} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} \coqdocvar{x} \ensuremath{\Rightarrow} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} (\coqref{Coqdoc.details.idnat:2}{\coqdocdefinition{idnat}} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}})\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} 0 \ensuremath{\Rightarrow} 0\coqdoceol +\coqdocindent{1.00em} +\coqdockw{end}.\coqdoceol +\end{coqdoccode} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/details.v b/test-suite/coqdoc/details.v new file mode 100644 index 0000000000..208e60317d --- /dev/null +++ b/test-suite/coqdoc/details.v @@ -0,0 +1,11 @@ +(* begin details *) +Definition foo : nat := 3. +(* end details *) + +(* begin details : Foo bar *) +Fixpoint idnat (x : nat) : nat := + match x with + | S x => S (idnat x) + | 0 => 0 + end. +(* end details *) -- cgit v1.2.3