From 3f2742b2c3fd48706d4bfd8bffdd4ae07a338bbd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 6 Apr 2020 10:04:42 +0200 Subject: Coqdoc: Exporting location and unique id for binding variables. This provides linking, appropriate coloring and appropriate hovering in coqdoc documents. In particular, this fixes #7697. --- test-suite/coqdoc/binder.html.out | 41 +++++++++++++++++++++++++++++++++++++ test-suite/coqdoc/binder.tex.out | 28 +++++++++++++++++++++++++ test-suite/coqdoc/binder.v | 3 +++ test-suite/coqdoc/bug11353.html.out | 6 +++--- test-suite/coqdoc/bug11353.tex.out | 6 +++--- test-suite/coqdoc/bug5648.html.out | 4 ++-- test-suite/coqdoc/bug5648.tex.out | 4 ++-- test-suite/coqdoc/links.html.out | 12 +++++------ test-suite/coqdoc/links.tex.out | 12 +++++------ 9 files changed, 94 insertions(+), 22 deletions(-) create mode 100644 test-suite/coqdoc/binder.html.out create mode 100644 test-suite/coqdoc/binder.tex.out create mode 100644 test-suite/coqdoc/binder.v (limited to 'test-suite') diff --git a/test-suite/coqdoc/binder.html.out b/test-suite/coqdoc/binder.html.out new file mode 100644 index 0000000000..a8ec7ae033 --- /dev/null +++ b/test-suite/coqdoc/binder.html.out @@ -0,0 +1,41 @@ + + + + + +Coqdoc.binder + + + + +
+ + + +
+ +

Library Coqdoc.binder

+ +
+
+ +
+Link binders +
+
+ +
+Definition foo alpha beta := alpha + beta.
+
+
+ + + +
+ + + \ No newline at end of file diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out new file mode 100644 index 0000000000..2b5648aee6 --- /dev/null +++ b/test-suite/coqdoc/binder.tex.out @@ -0,0 +1,28 @@ +\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.binder}{Library }{Coqdoc.binder} + +\begin{coqdoccode} +\end{coqdoccode} +Link binders \begin{coqdoccode} +\coqdocemptyline +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.binder.foo}{foo}{\coqdocdefinition{foo}} \coqdef{Coqdoc.binder.alpha:1}{alpha}{\coqdocbinder{alpha}} \coqdef{Coqdoc.binder.beta:2}{beta}{\coqdocbinder{beta}} := \coqref{Coqdoc.binder.alpha:1}{\coqdocvariable{alpha}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.binder.beta:2}{\coqdocvariable{beta}}.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/binder.v b/test-suite/coqdoc/binder.v new file mode 100644 index 0000000000..283ef64ac5 --- /dev/null +++ b/test-suite/coqdoc/binder.v @@ -0,0 +1,3 @@ +(** Link binders *) + +Definition foo alpha beta := alpha + beta. diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out index 0b4b4b6e37..7a1de45e6e 100644 --- a/test-suite/coqdoc/bug11353.html.out +++ b/test-suite/coqdoc/bug11353.html.out @@ -20,9 +20,9 @@
Definition a := 0. #[ universes( template) ]
-Inductive mysum (A B:Type) : Type :=
-  | myinl : A → mysum A B
-  | myinr : B → mysum A B.
+Inductive mysum (A B:Type) : Type :=
+  | myinl : A → mysum A B
+  | myinr : B → mysum A B.

#[local]Definition b := 1.
diff --git a/test-suite/coqdoc/bug11353.tex.out b/test-suite/coqdoc/bug11353.tex.out index a6478682d8..12ea109d0e 100644 --- a/test-suite/coqdoc/bug11353.tex.out +++ b/test-suite/coqdoc/bug11353.tex.out @@ -22,11 +22,11 @@ \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug11353.a}{a}{\coqdocdefinition{a}} := 0. \#[ \coqdocvar{universes}( \coqdocvar{template}) ]\coqdoceol \coqdocnoindent -\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdocvar{A} \coqdocvar{B}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol +\coqdockw{Inductive} \coqdef{Coqdoc.bug11353.mysum}{mysum}{\coqdocinductive{mysum}} (\coqdef{Coqdoc.bug11353.A:1}{A}{\coqdocbinder{A}} \coqdef{Coqdoc.bug11353.B:2}{B}{\coqdocbinder{B}}:\coqdockw{Type}) : \coqdockw{Type} :=\coqdoceol \coqdocindent{1.00em} -\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqdocvariable{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}\coqdoceol +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinl}{myinl}{\coqdocconstructor{myinl}} : \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}\coqdoceol \coqdocindent{1.00em} -\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqdocvariable{B} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum}{\coqdocinductive{mysum}} \coqdocvariable{A} \coqdocvariable{B}.\coqdoceol +\ensuremath{|} \coqdef{Coqdoc.bug11353.myinr}{myinr}{\coqdocconstructor{myinr}} : \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqref{Coqdoc.bug11353.mysum:3}{\coqdocinductive{mysum}} \coqref{Coqdoc.bug11353.A:1}{\coqdocvariable{A}} \coqref{Coqdoc.bug11353.B:2}{\coqdocvariable{B}}.\coqdoceol \coqdocemptyline \coqdocnoindent \#[\coqdocvar{local}]\coqdockw{Definition} \coqdef{Coqdoc.bug11353.b}{b}{\coqdocdefinition{b}} := 1.\coqdoceol diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out index 5c5a2dc299..8201cd3ccb 100644 --- a/test-suite/coqdoc/bug5648.html.out +++ b/test-suite/coqdoc/bug5648.html.out @@ -29,8 +29,8 @@ | A | Add | G | Goal | L | Lemma | P | Proof .

-Definition d x :=
-  match x with
+Definition d x :=
+  match x with
  | A ⇒ 0
  | Add ⇒ 1
  | G ⇒ 2
diff --git a/test-suite/coqdoc/bug5648.tex.out b/test-suite/coqdoc/bug5648.tex.out index 82f7da2309..c221d7ca8a 100644 --- a/test-suite/coqdoc/bug5648.tex.out +++ b/test-suite/coqdoc/bug5648.tex.out @@ -34,9 +34,9 @@ \ensuremath{|} \coqdef{Coqdoc.bug5648.A}{A}{\coqdocconstructor{A}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Add}{Add}{\coqdocconstructor{Add}} \ensuremath{|} \coqdef{Coqdoc.bug5648.G}{G}{\coqdocconstructor{G}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Goal}{Goal}{\coqdocconstructor{Goal}} \ensuremath{|} \coqdef{Coqdoc.bug5648.L}{L}{\coqdocconstructor{L}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Lemma}{Lemma}{\coqdocconstructor{Lemma}} \ensuremath{|} \coqdef{Coqdoc.bug5648.P}{P}{\coqdocconstructor{P}} \ensuremath{|} \coqdef{Coqdoc.bug5648.Proof}{Proof}{\coqdocconstructor{Proof}} .\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdocvar{x} :=\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.bug5648.d}{d}{\coqdocdefinition{d}} \coqdef{Coqdoc.bug5648.x:3}{x}{\coqdocbinder{x}} :=\coqdoceol \coqdocindent{1.00em} -\coqdockw{match} \coqdocvariable{x} \coqdockw{with}\coqdoceol +\coqdockw{match} \coqref{Coqdoc.bug5648.x:3}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol \coqdocindent{1.00em} \ensuremath{|} \coqref{Coqdoc.bug5648.A}{\coqdocconstructor{A}} \ensuremath{\Rightarrow} 0\coqdoceol \coqdocindent{1.00em} diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index d2d4d5d764..3ec5e7eb23 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -54,10 +54,10 @@ Various checks for coqdoc Definition g := "dfjkh""sdfhj forall <> * ~"%string.

-Definition a (b: nat) := b.
+Definition a (b: nat) := b.

-Definition f := ∀ C:Prop, C.
+Definition f := ∀ C:Prop, C.

Notation "n ++ m" := (plus n m).
@@ -74,9 +74,9 @@ Various checks for coqdoc Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).

-Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A
+Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A

-where "x = y :> A" := (@eq A x y) : type_scope.
+where "x = y :> A" := (@eq A x y) : type_scope.

Definition eq0 := 0 = 0 :> nat.
@@ -109,7 +109,7 @@ Various checks for coqdoc     Definition α := (0 + l)%my.

-    Definition a' b := b'++0++b2 _ ++x b.
+    Definition a' b := b'++0++b2 _ ++x b.

    Definition c := {True}+{True}.
@@ -137,7 +137,7 @@ Various checks for coqdoc       Variables b2: nat.

-      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.
+      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.

    End test.
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 24f96ff1e6..2304f5ecc1 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -45,10 +45,10 @@ Various checks for coqdoc \coqdockw{Definition} \coqdef{Coqdoc.links.g}{g}{\coqdocdefinition{g}} := "dfjkh""sdfhj forall <> * \~{}"\%\coqdocvar{string}.\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdocvar{b}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqdocvariable{b}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.a}{a}{\coqdocdefinition{a}} (\coqdef{Coqdoc.links.b:1}{b}{\coqdocbinder{b}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) := \coqref{Coqdoc.links.b:1}{\coqdocvariable{b}}.\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdef{Coqdoc.links.C:2}{C}{\coqdocbinder{C}}:\coqdockw{Prop}, \coqref{Coqdoc.links.C:2}{\coqdocvariable{C}}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol @@ -65,11 +65,11 @@ Various checks for coqdoc \coqdockw{Notation} \coqdef{Coqdoc.links.:::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol \coqdocemptyline \coqdocnoindent -\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol +\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdef{Coqdoc.links.A:3}{A}{\coqdocbinder{A}}:\coqdockw{Type}) (\coqdef{Coqdoc.links.x:4}{x}{\coqdocbinder{x}}:\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqref{Coqdoc.links.x:4}{\coqdocvariable{x}} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqref{Coqdoc.links.A:3}{\coqdocvariable{A}}\coqdoceol \coqdocnoindent \coqdoceol \coqdocnoindent -\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol +\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq:6}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol \coqdocemptyline \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol @@ -102,7 +102,7 @@ Various checks for coqdoc \coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.::my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdef{Coqdoc.links.b:9}{b}{\coqdocbinder{b}} := \coqref{Coqdoc.links.test.b'}{\coqdocvariable{b'}}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.test.b2}{\coqdocvariable{b2}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqref{Coqdoc.links.b:9}{\coqdocvariable{b}}.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} \coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol @@ -131,7 +131,7 @@ Various checks for coqdoc \coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol \coqdocemptyline \coqdocindent{3.00em} -\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol +\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdef{Coqdoc.links.b:12}{b}{\coqdocbinder{b}} := \coqref{Coqdoc.links.test2.b'}{\coqdocvariable{b'}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.test2.test.b2}{\coqdocvariable{b2}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqref{Coqdoc.links.b:12}{\coqdocvariable{b}} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol \coqdocemptyline \coqdocindent{2.00em} \coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol -- cgit v1.2.3