diff options
Diffstat (limited to 'test-suite')
37 files changed, 412 insertions, 93 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index eade52b6eb..954a922c8c 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -354,8 +354,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primit } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ - $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \ + $(coqchk) -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ @@ -381,7 +380,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ @@ -405,7 +404,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) } > "$@" @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi $(HIDE)if ! grep -q -F "Error!" $@; then { \ - $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ + $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ diff --git a/test-suite/bugs/closed/bug_11783.v b/test-suite/bugs/closed/bug_11783.v new file mode 100644 index 0000000000..a07391add5 --- /dev/null +++ b/test-suite/bugs/closed/bug_11783.v @@ -0,0 +1,5 @@ +Section S. + Variable A : Type. + Require Hurkens. + Definition foo := Hurkens.Generic.paradox A. +End S. diff --git a/test-suite/bugs/closed/bug_11935.v b/test-suite/bugs/closed/bug_11935.v new file mode 100644 index 0000000000..ad5ffc68b5 --- /dev/null +++ b/test-suite/bugs/closed/bug_11935.v @@ -0,0 +1,6 @@ +Section S. + Variable A : Prop. + + Fail Check A@{Type}. + Check A@{}. +End S. diff --git a/test-suite/bugs/closed/bug_12045.v b/test-suite/bugs/closed/bug_12045.v new file mode 100644 index 0000000000..4e416778a9 --- /dev/null +++ b/test-suite/bugs/closed/bug_12045.v @@ -0,0 +1,19 @@ +(* Check enough reduction happens in the conclusion of an induction scheme *) + +Lemma foo : + forall (P : nat -> Prop), + (forall n, P (S n)) -> + forall n, + (fun e => + IsSucc e -> + P e) n. +Proof. +Admitted. + +Theorem bar : forall n, + IsSucc n -> + True. +Proof. + intros. + Fail induction n using foo. (* was an anomaly *) +Admitted. diff --git a/test-suite/bugs/closed/bug_1912.v b/test-suite/bugs/closed/bug_1912.v index 987a541778..0228abbb9b 100644 --- a/test-suite/bugs/closed/bug_1912.v +++ b/test-suite/bugs/closed/bug_1912.v @@ -1,4 +1,4 @@ -Require Import ZArith. +Require Import Omega. Goal forall x, Z.succ (Z.pred x) = x. intros x. diff --git a/test-suite/bugs/closed/bug_7812.v b/test-suite/bugs/closed/bug_7812.v new file mode 100644 index 0000000000..a714eea81d --- /dev/null +++ b/test-suite/bugs/closed/bug_7812.v @@ -0,0 +1,30 @@ +Module Foo. + Definition binary A := A -> A -> Prop. + + Definition inter A (R1 R2 : binary A): binary A := + fun (x y:A) => R1 x y /\ R2 x y. +End Foo. + +Module Simple_sparse_proof. + Parameter node : Type. + Parameter graph : Type. + Parameter has_edge : graph -> node -> node -> Prop. + Implicit Types x y z : node. + Implicit Types G : graph. + + Parameter mem : forall A, A -> list A -> Prop. + Hypothesis mem_nil : forall x, mem node x nil = False. + + Definition notin (l: list node): node -> node -> Prop := + fun x y => ~ mem node x l /\ ~ mem node y l. + + Definition edge_notin G l : node -> node -> Prop := + Foo.inter node (has_edge G) (notin l). + + Hint Unfold Foo.inter notin edge_notin : rel_crush. + + Lemma edge_notin_nil G : forall x y, edge_notin G nil x y <-> has_edge G x y. + Proof. + intros. autounfold with rel_crush. rewrite !mem_nil. tauto. + Qed. +End Simple_sparse_proof. diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject index 3dfca7ffc0..85276fd9b9 100644 --- a/test-suite/coq-makefile/native1/_CoqProject +++ b/test-suite/coq-makefile/native1/_CoqProject @@ -1,6 +1,8 @@ -R src test -R theories test -I src +-arg -w +-arg +native-compiler-disabled -arg -native-compiler -arg yes diff --git a/test-suite/coq-makefile/native2/run.sh b/test-suite/coq-makefile/native2/run.sh index 857f70fdff..aaae81630f 100755 --- a/test-suite/coq-makefile/native2/run.sh +++ b/test-suite/coq-makefile/native2/run.sh @@ -7,7 +7,7 @@ if [[ $(which ocamlopt) && ! $NONATIVECOMP ]]; then coq_makefile -f _CoqProject -o Makefile cat Makefile.conf -COQEXTRAFLAGS="-native-compiler yes" make +COQEXTRAFLAGS="-w +native-compiler-disabled -native-compiler yes" make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug 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 7900c034da..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,15 +1,5 @@ -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQDEP VFILES -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' 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) -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' +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 7ab0bc75d9..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,15 +1,5 @@ -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' COQDEP VFILES -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' 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) -Makefile:69: warning: undefined variable '*' -Makefile:204: warning: undefined variable 'DSTROOT' +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/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 4ee4aae36c..f556638640 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -63,7 +63,7 @@ TO_SED_IN_PER_LINE=( for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do for ext in "" .desired; do - grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed + sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" ${file}${ext} > ${file}${ext}.processed done echo "cat $file" cat "$file" diff --git a/test-suite/coqdoc/binder.html.out b/test-suite/coqdoc/binder.html.out new file mode 100644 index 0000000000..af8eb46845 --- /dev/null +++ b/test-suite/coqdoc/binder.html.out @@ -0,0 +1,41 @@ +<!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.binder</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.binder</h1> + +<div class="code"> +</div> + +<div class="doc"> +Link binders +</div> +<div class="code"> + +<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> + +<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/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/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 0b4b4b6e37..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> (<span class="id" title="var">A</span> <span class="id" title="var">B</span>:<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"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><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"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="Coqdoc.bug11353.html#mysum"><span class="id" title="inductive">mysum</span></a> <a class="idref" href="Coqdoc.bug11353.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="Coqdoc.bug11353.html#B"><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/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..e1d1c1313e 100644 --- a/test-suite/coqdoc/bug5648.html.out +++ b/test-suite/coqdoc/bug5648.html.out @@ -19,18 +19,18 @@ <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> <span class="id" title="var">x</span> :=<br/> - <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.bug5648.html#x"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><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/> | <a class="idref" href="Coqdoc.bug5648.html#G"><span class="id" title="constructor">G</span></a> ⇒ 2<br/> 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/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 d2d4d5d764..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> (<span class="id" title="var">b</span>: <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"><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> <span class="id" title="var">C</span>:<span class="id" title="keyword">Prop</span>, <a class="idref" href="Coqdoc.links.html#C"><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> (<span class="id" title="var">A</span>:<span class="id" title="keyword">Type</span>) (<span class="id" title="var">x</span>:<a class="idref" href="Coqdoc.links.html#A"><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#1c93e43e07fbeaeb6a625cb6614beb5d"><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"><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"><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"><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"><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> <span class="id" title="var">b</span> := <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"><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> <span class="id" title="var">b</span> := <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"><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/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 diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index abc7f0f88e..e0aa758812 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -2,9 +2,9 @@ The command has indeed failed with message: Flag "rename" expected to rename A into B. File "stdin", line 3, characters 0-25: Warning: This command is just asserting the names of arguments of identity. -If this is what you want add ': assert' to silence the warning. If you want -to clear implicit arguments add ': clear implicits'. If you want to clear -notation scopes add ': clear scopes' [arguments-assert,vernacular] +If this is what you want, add ': assert' to silence the warning. If you want +to clear implicit arguments, add ': clear implicits'. If you want to clear +notation scopes, add ': clear scopes' [arguments-assert,vernacular] @eq_refl : forall (B : Type) (y : B), y = y eq_refl diff --git a/test-suite/output/NotationsSigma.out b/test-suite/output/NotationsSigma.out new file mode 100644 index 0000000000..0e4df87148 --- /dev/null +++ b/test-suite/output/NotationsSigma.out @@ -0,0 +1,40 @@ +{0 = 0} + {0 < 1} + : Set +(0 = 0) + {0 < 1} + : Set +{x : nat | x = 1} + : Set +{x : nat | x = 1 & 0 < x} + : Set +{x : nat | x = 1} + : Set +{x : nat | x = 1 & 0 < x} + : Set +{x : nat & x = 1} + : Set +{x : nat & x = 1 & 0 < x} + : Set +{x : nat & x = 1} + : Set +{x : nat & x = 1 & 0 < x} + : Set +{'(x, _) : nat * ?T | x = 1} + : Type +where +?T : [pat : nat * ?T |- Type] (pat cannot be used) +{'(x, y) : nat * nat | x = 1 & y = 0} + : Set +{'(x, _) : nat * nat | x = 1} + : Set +{'(x, y) : nat * nat | x = 1 & y = 0} + : Set +{'(x, _) : nat * ?T & x = 1} + : Type +where +?T : [pat : nat * ?T |- Type] (pat cannot be used) +{'(x, y) : nat * nat & x = 1 & y = 0} + : Type +{'(x, _) : nat * nat & x = 1} + : Type +{'(x, y) : nat * nat & x = 1 & y = 0} + : Type diff --git a/test-suite/output/NotationsSigma.v b/test-suite/output/NotationsSigma.v new file mode 100644 index 0000000000..6780d63a04 --- /dev/null +++ b/test-suite/output/NotationsSigma.v @@ -0,0 +1,22 @@ +(* Check notations for sigma types *) + +Check { 0 = 0 } + { 0 < 1 }. +Check (0 = 0) + { 0 < 1 }. + +Check { x | x = 1 }. +Check { x | x = 1 & 0 < x }. +Check { x : nat | x = 1 }. +Check { x : nat | x = 1 & 0 < x }. +Check { x & x = 1 }. +Check { x & x = 1 & 0 < x }. +Check { x : nat & x = 1 }. +Check { x : nat & x = 1 & 0 < x }. + +Check {'(x,y) | x = 1 }. +Check {'(x,y) | x = 1 & y = 0 }. +Check {'(x,y) : nat * nat | x = 1 }. +Check {'(x,y) : nat * nat | x = 1 & y = 0 }. +Check {'(x,y) & x = 1 }. +Check {'(x,y) & x = 1 & y = 0 }. +Check {'(x,y) : nat * nat & x = 1 }. +Check {'(x,y) : nat * nat & x = 1 & y = 0 }. diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out index e9c28faf1d..1dd89c9bcd 100644 --- a/test-suite/output/Projections.out +++ b/test-suite/output/Projections.out @@ -1,2 +1,17 @@ fun S : store => S.(store_funcs) : store -> host_func +a = +fun A : Type => +let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u) + : forall A : Type, + let B := A in + forall C : Type, U A C -> Type * Type * Type * (B * A * C) + +Arguments a (_ _)%type_scope +b = +fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u + : forall A : Type, + let B := A in + forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u) + +Arguments b (_ _)%type_scope diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v index 14d63d39c4..83a581338f 100644 --- a/test-suite/output/Projections.v +++ b/test-suite/output/Projections.v @@ -10,3 +10,12 @@ Section store. End store. Check (fun (S:@store nat) => S.(store_funcs)). + +Module LocalDefUnfolding. + +Unset Printing Projections. +Record U A (B:=A) C := {c:B*A*C;a:=(A,B,C,c);b:a=a}. +Print a. +Print b. + +End LocalDefUnfolding. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 9d8e830d64..593d0c7f67 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -136,7 +136,7 @@ h': newdef n <> n (use "About" for full details on implicit arguments) (use "About" for full details on implicit arguments) The command has indeed failed with message: -No such goal. +[Focus] No such goal. The command has indeed failed with message: Query commands only support the single numbered goal selector. The command has indeed failed with message: diff --git a/test-suite/output/UselessSyndef.out b/test-suite/output/UselessSyndef.out new file mode 100644 index 0000000000..ce484889b3 --- /dev/null +++ b/test-suite/output/UselessSyndef.out @@ -0,0 +1,2 @@ +a + : nat diff --git a/test-suite/output/UselessSyndef.v b/test-suite/output/UselessSyndef.v new file mode 100644 index 0000000000..96ad6e9f5c --- /dev/null +++ b/test-suite/output/UselessSyndef.v @@ -0,0 +1,10 @@ +Module M. + Definition a := 0. +End M. +Module N. + Notation a := M.a (only parsing). +End N. + +Import M. Import N. + +Check a. diff --git a/test-suite/output/bug_11934.out b/test-suite/output/bug_11934.out new file mode 100644 index 0000000000..072136c82e --- /dev/null +++ b/test-suite/output/bug_11934.out @@ -0,0 +1,13 @@ +thing = forall x y : foo, bla x y + : Prop +thing = +forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y + : Prop +(* {thing.u1 thing.u0} |= bla.u0 = thing.u0 + bla.u1 = thing.u1 *) +thing = +forall (x : @foo@{thing.u0} True) (y : @foo@{thing.u1} True), +@bla True True x y + : Prop +(* {thing.u1 thing.u0} |= bla.u0 = thing.u0 + bla.u1 = thing.u1 *) diff --git a/test-suite/output/bug_11934.v b/test-suite/output/bug_11934.v new file mode 100644 index 0000000000..fe9772dc62 --- /dev/null +++ b/test-suite/output/bug_11934.v @@ -0,0 +1,13 @@ +Polymorphic Axiom foo@{u} : Prop -> Prop. +Arguments foo {_}. + +Axiom bla : forall {A B}, @foo A -> @foo B -> Prop. +Definition thing := forall (x:@foo@{Type} True) (y:@foo@{Type} True), bla x y. + +Print thing. (* forall x y : foo, bla x y *) + +Set Printing Universes. +Print thing. (* forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y *) + +Set Printing Implicit. +Print thing. (* BAD: forall x y : @foo@{thing.u0} True, @bla True True x y *) diff --git a/test-suite/output/undeclared_key.out b/test-suite/output/undeclared_key.out new file mode 100644 index 0000000000..ed768751fc --- /dev/null +++ b/test-suite/output/undeclared_key.out @@ -0,0 +1,13 @@ +The command has indeed failed with message: +There is no flag, option or table with this name: "Search Blacklists". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". +File "stdin", line 3, characters 0-22: +Warning: There is no flag or option with this name: "Search Blacklists". +[unknown-option,option] +The command has indeed failed with message: +There is no string-valued table with this name: "Search Blacklists". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". +The command has indeed failed with message: +There is no qualid-valued table with this name: "Search Blacklist". diff --git a/test-suite/output/undeclared_key.v b/test-suite/output/undeclared_key.v new file mode 100644 index 0000000000..4134bc8bfa --- /dev/null +++ b/test-suite/output/undeclared_key.v @@ -0,0 +1,6 @@ +Fail Test Search Blacklists. +Fail Test Search Blacklist for foo. +Set Search Blacklists. +Fail Remove Search Blacklists "bar" foo. +Fail Remove Search Blacklist "bar" foo. +Fail Add Search Blacklist "bar" foo. diff --git a/test-suite/success/PartialImport.v b/test-suite/success/PartialImport.v new file mode 100644 index 0000000000..720083aec5 --- /dev/null +++ b/test-suite/success/PartialImport.v @@ -0,0 +1,58 @@ +Module M. + + Definition a := 0. + Definition b := 1. + + Module N. + + Notation c := (a + b). + + End N. + + Inductive even : nat -> Prop := + | even_0 : even 0 + | even_S n : odd n -> even (S n) + with odd : nat -> Set := + odd_S n : even n -> odd (S n). + +End M. + +Module Simple. + + Import M(a). + + Check a. + Fail Check b. + Fail Check N.c. + + (* todo output test: this prints a+M.b since the notation isn't imported *) + Check M.N.c. + + Fail Import M(c). + Fail Import M(M.b). + + Import M(N.c). + Check N.c. + (* interestingly prints N.c (also does with unfiltered Import M) *) + + Import M(even(..)). + Check even. Check even_0. Check even_S. + Check even_sind. Check even_ind. + Fail Check even_rect. (* doesn't exist *) + Fail Check odd. Check M.odd. + Fail Check odd_S. Fail Check odd_sind. + +End Simple. + +Module WithExport. + + Module X. + Export M(a, N.c). + End X. + + Import X. + Check a. + Check N.c. (* also prints N.c *) + Fail Check b. + +End WithExport. diff --git a/test-suite/success/let_universes.v b/test-suite/success/let_universes.v new file mode 100644 index 0000000000..c780ec010f --- /dev/null +++ b/test-suite/success/let_universes.v @@ -0,0 +1,5 @@ +Section S. +Let bla@{} := Prop. +Let bli@{u} := Type@{u}. +Fail Let blo@{} := Type. +End S. |