diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/08-tools/12091-master+coqdoc-css-target.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/08-tools/12126-adjust-timed-name.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 16 | ||||
| -rw-r--r-- | test-suite/coq-makefile/timing/after/time-of-build-after.log.desired | 4 | ||||
| -rw-r--r-- | test-suite/coq-makefile/timing/after/time-of-build-before.log.desired | 4 | ||||
| -rw-r--r-- | test-suite/coq-makefile/timing/after/time-of-build-both.log.desired | 4 | ||||
| -rw-r--r-- | test-suite/coqdoc/binder.html.out | 2 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug11194.html.out | 10 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug11353.html.out | 10 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5648.html.out | 8 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.html.out | 4 | ||||
| -rw-r--r-- | test-suite/coqdoc/links.html.out | 56 | ||||
| -rw-r--r-- | tools/CoqMakefile.in | 2 | ||||
| -rw-r--r-- | tools/coqdoc/coqdoc.css | 5 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 3 |
17 files changed, 84 insertions, 62 deletions
diff --git a/Makefile.build b/Makefile.build index 7879580e18..8a8500ba1a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -201,7 +201,7 @@ DEPENDENCIES := \ # Default timing command # Use /usr/bin/env time on linux, gtime on Mac OS -TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) ifeq (0,$(shell /usr/bin/env time -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=/usr/bin/env time -f $(TIMEFMT) diff --git a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst new file mode 100644 index 0000000000..5c4ef82b8b --- /dev/null +++ b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst @@ -0,0 +1,4 @@ +- **Added:** + Definitions in coqdoc link to themselves, giving access in html to their own url + (`#12026 <https://github.com/coq/coq/pull/12026>`_, + by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_). diff --git a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst new file mode 100644 index 0000000000..f6af5d40e8 --- /dev/null +++ b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst @@ -0,0 +1,4 @@ +- **Added:** + ``Coqdoc``: Highlighting of the exact position of the target of links + (`#12091 <https://github.com/coq/coq/pull/12091>`_, + by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12126-adjust-timed-name.rst b/doc/changelog/08-tools/12126-adjust-timed-name.rst new file mode 100644 index 0000000000..c305b384d9 --- /dev/null +++ b/doc/changelog/08-tools/12126-adjust-timed-name.rst @@ -0,0 +1,8 @@ +- **Changed:** + The output of ``make TIMED=1`` (and therefore the timing targets + such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now + displays the full name of the output file being built, rather than + the stem of the rule (which was usually the filename without the + extension, but in general could be anything for user-defined rules + involving ``%``) (`#12126 + <https://github.com/coq/coq/pull/12126>`_, by Jason Gross). diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 921c7bbbf7..bc77e2e58c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -245,9 +245,9 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.34 mem: 395448 ko) + Slow.vo (user: 0.34 mem: 395448 ko) COQC Fast.v - Fast (user: 0.01 mem: 45184 ko) + Fast.vo (user: 0.01 mem: 45184 ko) + ``pretty-timed`` this target stores the output of ``make TIMED=1`` into @@ -280,15 +280,15 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.36 mem: 393912 ko) + Slow.vo (user: 0.36 mem: 393912 ko) COQC Fast.v - Fast (user: 0.05 mem: 45992 ko) + Fast.vo (user: 0.05 mem: 45992 ko) Time | File Name -------------------- 0m00.41s | Total -------------------- - 0m00.36s | Slow - 0m00.05s | Fast + 0m00.36s | Slow.vo + 0m00.05s | Fast.vo + ``print-pretty-timed-diff`` @@ -338,8 +338,8 @@ file timing data: -------------------------------------------------------- 0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% -------------------------------------------------------- - 0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% - 0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% + 0m00.37s | Slow.vo | 0m00.01s || +0m00.36s | +3600.00% + 0m00.02s | Fast.vo | 0m00.34s || -0m00.32s | -94.11% The following targets and ``Makefile`` variables allow collection of per- diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired index 4381160a4e..ebe44f3548 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -1,5 +1,5 @@ COQDEP VFILES COQC Slow.v -Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) +Slow.vo (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) COQC Fast.v -Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) +Fast.vo (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired index e6af909268..bf17a3e95c 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -1,5 +1,5 @@ COQDEP VFILES COQC Slow.v -Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) +Slow.vo (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) COQC Fast.v -Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) +Fast.vo (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired index 72c520218c..c8f35dc1e4 100644 --- a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -2,5 +2,5 @@ After | File Name | Before || Change | % Change -------------------------------------------------------- 0m00.34s | Total | 0m00.49s || -0m00.14s | -30.61% -------------------------------------------------------- -0m00.32s | Fast | 0m00.02s || +0m00.30s | +1500.00% -0m00.02s | Slow | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file +0m00.32s | Fast.vo | 0m00.02s || +0m00.30s | +1500.00% +0m00.02s | Slow.vo | 0m00.47s || -0m00.44s | -95.74%
\ No newline at end of file diff --git a/test-suite/coqdoc/binder.html.out b/test-suite/coqdoc/binder.html.out index a8ec7ae033..af8eb46845 100644 --- a/test-suite/coqdoc/binder.html.out +++ b/test-suite/coqdoc/binder.html.out @@ -27,7 +27,7 @@ Link binders <div class="code"> <br/> -<span class="id" title="keyword">Definition</span> <a name="foo"><span class="id" title="definition">foo</span></a> <a name="alpha:1"><span class="id" title="binder">alpha</span></a> <a name="beta:2"><span class="id" title="binder">beta</span></a> := <a class="idref" href="Coqdoc.binder.html#alpha:1"><span class="id" title="variable">alpha</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.binder.html#beta:2"><span class="id" title="variable">beta</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="foo" class="idref" href="#foo"><span class="id" title="definition">foo</span></a> <a id="alpha:1" class="idref" href="#alpha:1"><span class="id" title="binder">alpha</span></a> <a id="beta:2" class="idref" href="#beta:2"><span class="id" title="binder">beta</span></a> := <a class="idref" href="Coqdoc.binder.html#alpha:1"><span class="id" title="variable">alpha</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.binder.html#beta:2"><span class="id" title="variable">beta</span></a>.<br/> </div> </div> diff --git a/test-suite/coqdoc/bug11194.html.out b/test-suite/coqdoc/bug11194.html.out index 304d041033..6fc6533e59 100644 --- a/test-suite/coqdoc/bug11194.html.out +++ b/test-suite/coqdoc/bug11194.html.out @@ -19,11 +19,11 @@ <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/> +<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">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/> </div> </div> diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out index 7a1de45e6e..f9d6a79906 100644 --- a/test-suite/coqdoc/bug11353.html.out +++ b/test-suite/coqdoc/bug11353.html.out @@ -19,13 +19,13 @@ <h1 class="libtitle">Library Coqdoc.bug11353</h1> <div class="code"> -<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> := 0. #[ <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/> -<span class="id" title="keyword">Inductive</span> <a name="mysum"><span class="id" title="inductive">mysum</span></a> (<a name="A:1"><span class="id" title="binder">A</span></a> <a name="B:2"><span class="id" title="binder">B</span></a>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/> - | <a name="myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a><br/> - | <a name="myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="a" class="idref" href="#a"><span class="id" title="definition">a</span></a> := 0. #[ <span class="id" title="var">universes</span>( <span class="id" title="var">template</span>) ]<br/> +<span class="id" title="keyword">Inductive</span> <a id="mysum" class="idref" href="#mysum"><span class="id" title="inductive">mysum</span></a> (<a id="A:1" class="idref" href="#A:1"><span class="id" title="binder">A</span></a> <a id="B:2" class="idref" href="#B:2"><span class="id" title="binder">B</span></a>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/> + | <a id="myinl" class="idref" href="#myinl"><span class="id" title="constructor">myinl</span></a> : <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a><br/> + | <a id="myinr" class="idref" href="#myinr"><span class="id" title="constructor">myinr</span></a> : <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum:3"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A:1"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B:2"><span class="id" title="variable">B</span></a>.<br/> <br/> -#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a name="b"><span class="id" title="definition">b</span></a> := 1.<br/> +#[<span class="id" title="var">local</span>]<span class="id" title="keyword">Definition</span> <a id="b" class="idref" href="#b"><span class="id" title="definition">b</span></a> := 1.<br/> </div> </div> diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out index 8201cd3ccb..e1d1c1313e 100644 --- a/test-suite/coqdoc/bug5648.html.out +++ b/test-suite/coqdoc/bug5648.html.out @@ -19,17 +19,17 @@ <h1 class="libtitle">Library Coqdoc.bug5648</h1> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="a"><span class="id" title="lemma">a</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a id="a" class="idref" href="#a"><span class="id" title="lemma">a</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a>.<br/> <span class="id" title="keyword">Proof</span>.<br/> <span class="id" title="tactic">auto</span>.<br/> <span class="id" title="keyword">Qed</span>.<br/> <br/> -<span class="id" title="keyword">Variant</span> <a name="t"><span class="id" title="inductive">t</span></a> :=<br/> -| <a name="A"><span class="id" title="constructor">A</span></a> | <a name="Add"><span class="id" title="constructor">Add</span></a> | <a name="G"><span class="id" title="constructor">G</span></a> | <a name="Goal"><span class="id" title="constructor">Goal</span></a> | <a name="L"><span class="id" title="constructor">L</span></a> | <a name="Lemma"><span class="id" title="constructor">Lemma</span></a> | <a name="P"><span class="id" title="constructor">P</span></a> | <a name="Proof"><span class="id" title="constructor">Proof</span></a> .<br/> +<span class="id" title="keyword">Variant</span> <a id="t" class="idref" href="#t"><span class="id" title="inductive">t</span></a> :=<br/> +| <a id="A" class="idref" href="#A"><span class="id" title="constructor">A</span></a> | <a id="Add" class="idref" href="#Add"><span class="id" title="constructor">Add</span></a> | <a id="G" class="idref" href="#G"><span class="id" title="constructor">G</span></a> | <a id="Goal" class="idref" href="#Goal"><span class="id" title="constructor">Goal</span></a> | <a id="L" class="idref" href="#L"><span class="id" title="constructor">L</span></a> | <a id="Lemma" class="idref" href="#Lemma"><span class="id" title="constructor">Lemma</span></a> | <a id="P" class="idref" href="#P"><span class="id" title="constructor">P</span></a> | <a id="Proof" class="idref" href="#Proof"><span class="id" title="constructor">Proof</span></a> .<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> <a name="x:3"><span class="id" title="binder">x</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 id="x:3" class="idref" href="#x:3"><span class="id" title="binder">x</span></a> :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x:3"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="Coqdoc.bug5648.html#A"><span class="id" title="constructor">A</span></a> ⇒ 0<br/> | <a class="idref" href="Coqdoc.bug5648.html#Add"><span class="id" title="constructor">Add</span></a> ⇒ 1<br/> diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index b96fc6281d..286e8bba4d 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -26,7 +26,7 @@ </div> <div class="code"> -<span class="id" title="keyword">Definition</span> <a name="const1"><span class="id" title="definition">const1</span></a> := 1.<br/> +<span class="id" title="keyword">Definition</span> <a id="const1" class="idref" href="#const1"><span class="id" title="definition">const1</span></a> := 1.<br/> <br/> </div> @@ -36,7 +36,7 @@ </div> <div class="code"> -<span class="id" title="keyword">Definition</span> <a name="const2"><span class="id" title="definition">const2</span></a> := 2.<br/> +<span class="id" title="keyword">Definition</span> <a id="const2" class="idref" href="#const2"><span class="id" title="definition">const2</span></a> := 2.<br/> </div> </div> diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index 3ec5e7eb23..12d284dc54 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -51,93 +51,93 @@ Various checks for coqdoc <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Strings.String.html#"><span class="id" title="library">String</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="g"><span class="id" title="definition">g</span></a> := "dfjkh""sdfhj forall <> * ~"%<span class="id" title="var">string</span>.<br/> +<span class="id" title="keyword">Definition</span> <a id="g" class="idref" href="#g"><span class="id" title="definition">g</span></a> := "dfjkh""sdfhj forall <> * ~"%<span class="id" title="var">string</span>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="a"><span class="id" title="definition">a</span></a> (<a name="b:1"><span class="id" title="binder">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 class="idref" href="Coqdoc.links.html#b:1"><span class="id" title="variable">b</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="a" class="idref" href="#a"><span class="id" title="definition">a</span></a> (<a id="b:1" class="idref" href="#b:1"><span class="id" title="binder">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 class="idref" href="Coqdoc.links.html#b:1"><span class="id" title="variable">b</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</span> <a name="C:2"><span class="id" title="binder">C</span></a>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C:2"><span class="id" title="variable">C</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="f" class="idref" href="#f"><span class="id" title="definition">f</span></a> := <span class="id" title="keyword">∀</span> <a id="C:2" class="idref" href="#C:2"><span class="id" title="binder">C</span></a>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C:2"><span class="id" title="variable">C</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> +<span class="id" title="keyword">Notation</span> <a id="f03f7a04ef75ff3ac66ca5c23554e52e" class="idref" href="#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). +<span class="id" title="keyword">Notation</span> <a id="f03f7a04ef75ff3ac66ca5c23554e52e" class="idref" href="#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">"</span></a>n ++ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#mult"><span class="id" title="abbreviation">mult</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>). <br/> -<span class="id" title="keyword">Notation</span> <a name="f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">"</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> +<span class="id" title="keyword">Notation</span> <a id="f07b3676d96b68749d342542fd80e2b0" class="idref" href="#f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">"</span></a>n ** m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">"</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> +<span class="id" title="keyword">Notation</span> <a id="a647c51c9816a1b44fcfa5312db8344a" class="idref" href="#a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">"</span></a>n ▵ m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> +<span class="id" title="keyword">Notation</span> <a id="3dd9eae9daa65efe5444f5fc3529a2e7" class="idref" href="#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">"</span></a>n '_' ++ 'x' m" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#plus"><span class="id" title="abbreviation">plus</span></a> <span class="id" title="var">n</span> <span class="id" title="var">m</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 3).<br/> <br/> -<span class="id" title="keyword">Inductive</span> <a name="eq"><span class="id" title="inductive">eq</span></a> (<a name="A:3"><span class="id" title="binder">A</span></a>:<span class="id" title="keyword">Type</span>) (<a name="x:4"><span class="id" title="binder">x</span></a>:<a class="idref" href="Coqdoc.links.html#A:3"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a name="eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x:4"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x:4"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A:3"><span class="id" title="variable">A</span></a><br/> +<span class="id" title="keyword">Inductive</span> <a id="eq" class="idref" href="#eq"><span class="id" title="inductive">eq</span></a> (<a id="A:3" class="idref" href="#A:3"><span class="id" title="binder">A</span></a>:<span class="id" title="keyword">Type</span>) (<a id="x:4" class="idref" href="#x:4"><span class="id" title="binder">x</span></a>:<a class="idref" href="Coqdoc.links.html#A:3"><span class="id" title="variable">A</span></a>) : <span class="id" title="var">A</span> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> := <a id="eq_refl" class="idref" href="#eq_refl"><span class="id" title="constructor">eq_refl</span></a> : <a class="idref" href="Coqdoc.links.html#x:4"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="Coqdoc.links.html#x:4"><span class="id" title="variable">x</span></a> <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a><a class="idref" href="Coqdoc.links.html#A:3"><span class="id" title="variable">A</span></a><br/> <br/> -<span class="id" title="keyword">where</span> <a name="b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq:6"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">where</span> <a id="b8b2ebc8e1a8b9aa935c0702efb5dccf" class="idref" href="#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">"</span></a>x = y :> A" := (@<a class="idref" href="Coqdoc.links.html#eq:6"><span class="id" title="inductive">eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">type_scope</span>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></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="eq0" class="idref" href="#eq0"><span class="id" title="definition">eq0</span></a> := 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 0 <a class="idref" href="Coqdoc.links.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></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/> <br/> -<span class="id" title="keyword">Notation</span> <a name="2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">"</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/> +<span class="id" title="keyword">Notation</span> <a id="2c0c193cd2aedf7ecdb713db64dbfce6" class="idref" href="#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">"</span></a>( x # y ; .. ; z )" := (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> .. (<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#pair"><span class="id" title="constructor">pair</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) .. <span class="id" title="var">z</span>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a id="9f5a1d89cbd4d38f5e289576db7123d1" class="idref" href="#9f5a1d89cbd4d38f5e289576db7123d1"><span class="id" title="definition">b_α</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">(</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">#</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">;</span></a>0<a class="idref" href="Coqdoc.links.html#2c0c193cd2aedf7ecdb713db64dbfce6"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0 <a class="idref" href="Coqdoc.links.html#f07b3676d96b68749d342542fd80e2b0"><span class="id" title="notation">**</span></a> 0<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">))</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a id="h" class="idref" href="#h"><span class="id" title="abbreviation">h</span></a> := <a class="idref" href="Coqdoc.links.html#a"><span class="id" title="definition">a</span></a>.<br/> <br/> - <span class="id" title="keyword">Section</span> <a name="test"><span class="id" title="section">test</span></a>.<br/> + <span class="id" title="keyword">Section</span> <a id="test" class="idref" href="#test"><span class="id" title="section">test</span></a>.<br/> <br/> - <span class="id" title="keyword">Variables</span> <a name="test.b'"><span class="id" title="variable">b'</span></a> <a name="test.b2"><span class="id" title="variable">b2</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">Variables</span> <a id="test.b'" class="idref" href="#test.b'"><span class="id" title="variable">b'</span></a> <a id="test.b2" class="idref" href="#test.b2"><span class="id" title="variable">b2</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/> <br/> - <span class="id" title="keyword">Notation</span> <a name="2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">"</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/> + <span class="id" title="keyword">Notation</span> <a id="2158f15740ce05a939b657be222c26d6" class="idref" href="#2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">"</span></a>n + m" := (<span class="id" title="var">n</span> <a class="idref" href="Coqdoc.links.html#a647c51c9816a1b44fcfa5312db8344a"><span class="id" title="notation">▵</span></a> <span class="id" title="var">m</span>) : <span class="id" title="var">my_scope</span>.<br/> <br/> <span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">my_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">my</span>.<br/> <br/> - <span class="id" title="keyword">Notation</span> <a name="l"><span class="id" title="abbreviation">l</span></a> := 0.<br/> + <span class="id" title="keyword">Notation</span> <a id="l" class="idref" href="#l"><span class="id" title="abbreviation">l</span></a> := 0.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/> + <span class="id" title="keyword">Definition</span> <a id="ab410a966ac148e9b78c65c6cdf301fd" class="idref" href="#ab410a966ac148e9b78c65c6cdf301fd"><span class="id" title="definition">α</span></a> := (0 <a class="idref" href="Coqdoc.links.html#2158f15740ce05a939b657be222c26d6"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#l"><span class="id" title="abbreviation">l</span></a>)%<span class="id" title="var">my</span>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="a'"><span class="id" title="definition">a'</span></a> <a name="b:9"><span class="id" title="binder">b</span></a> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b:9"><span class="id" title="variable">b</span></a>.<br/> + <span class="id" title="keyword">Definition</span> <a id="a'" class="idref" href="#a'"><span class="id" title="definition">a'</span></a> <a id="b:9" class="idref" href="#b:9"><span class="id" title="binder">b</span></a> := <a class="idref" href="Coqdoc.links.html#test.b'"><span class="id" title="variable">b'</span></a><a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a>0<a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a><a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b:9"><span class="id" title="variable">b</span></a>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a>.<br/> + <span class="id" title="keyword">Definition</span> <a id="c" class="idref" href="#c"><span class="id" title="definition">c</span></a> := <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}+{</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a><a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Specif.html#87727981cdc1579fef00b9d9c1d3b9da"><span class="id" title="notation">}</span></a>.<br/> <br/> - <span class="id" title="keyword">Definition</span> <a name="d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/> + <span class="id" title="keyword">Definition</span> <a id="d" class="idref" href="#d"><span class="id" title="definition">d</span></a> := (1<a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a>2)%<span class="id" title="var">nat</span>.<br/> <br/> - <span class="id" title="keyword">Lemma</span> <a name="e"><span class="id" title="lemma">e</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 class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</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">Lemma</span> <a id="e" class="idref" href="#e"><span class="id" title="lemma">e</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 class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#e03f39daf98516fa530d3f6f5a1b4d92"><span class="id" title="notation">+</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="var">Admitted</span>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test"><span class="id" title="section">test</span></a>.<br/> <br/> - <span class="id" title="keyword">Section</span> <a name="test2"><span class="id" title="section">test2</span></a>.<br/> + <span class="id" title="keyword">Section</span> <a id="test2" class="idref" href="#test2"><span class="id" title="section">test2</span></a>.<br/> <br/> - <span class="id" title="keyword">Variables</span> <a name="test2.b'"><span class="id" title="variable">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>.<br/> + <span class="id" title="keyword">Variables</span> <a id="test2.b'" class="idref" href="#test2.b'"><span class="id" title="variable">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>.<br/> <br/> - <span class="id" title="keyword">Section</span> <a name="test2.test"><span class="id" title="section">test</span></a>.<br/> + <span class="id" title="keyword">Section</span> <a id="test2.test" class="idref" href="#test2.test"><span class="id" title="section">test</span></a>.<br/> <br/> - <span class="id" title="keyword">Variables</span> <a name="test2.test.b2"><span class="id" title="variable">b2</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">Variables</span> <a id="test2.test.b2" class="idref" href="#test2.test.b2"><span class="id" title="variable">b2</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/> <br/> - <span class="id" title="keyword">Definition</span> <a name="a''"><span class="id" title="definition">a''</span></a> <a name="b:12"><span class="id" title="binder">b</span></a> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b:12"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/> + <span class="id" title="keyword">Definition</span> <a id="a''" class="idref" href="#a''"><span class="id" title="definition">a''</span></a> <a id="b:12" class="idref" href="#b:12"><span class="id" title="binder">b</span></a> := <a class="idref" href="Coqdoc.links.html#test2.b'"><span class="id" title="variable">b'</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#O"><span class="id" title="constructor">O</span></a> <a class="idref" href="Coqdoc.links.html#f03f7a04ef75ff3ac66ca5c23554e52e"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#test2.test.b2"><span class="id" title="variable">b2</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">_</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">++</span></a> <a class="idref" href="Coqdoc.links.html#3dd9eae9daa65efe5444f5fc3529a2e7"><span class="id" title="notation">x</span></a> <a class="idref" href="Coqdoc.links.html#b:12"><span class="id" title="variable">b</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Coqdoc.links.html#h"><span class="id" title="abbreviation">h</span></a> 0.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="Coqdoc.links.html#test2.test"><span class="id" title="section">test</span></a>.<br/> diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0202b3136b..745bbb7e55 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -66,7 +66,7 @@ VERBOSE ?= TIMED?= TIMECMD?= # Use command time on linux, gtime on Mac OS -TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=command time -f $(TIMEFMT) diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 2c2bd98541..48096e555a 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -331,3 +331,8 @@ ul.doclist { margin-top: 0em; margin-bottom: 0em; } + +.code :target { + border: 2px solid #D4D4D4; + background-color: #e5eecc; +} diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 04725aa26f..d6f51d7b78 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -659,7 +659,8 @@ module Html = struct let reference s r = match r with | Def (fullid,ty) -> - printf "<a name=\"%s\">" (sanitize_name fullid); + let s' = sanitize_name fullid in + printf "<a id=\"%s\" class=\"idref\" href=\"#%s\">" s' s'; printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s |