diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12566_1.v | 16 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug12742.html.out | 67 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug12742.tex.out | 51 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug12742.v | 20 | ||||
| -rw-r--r-- | test-suite/coqdoc/details.html.out | 48 | ||||
| -rw-r--r-- | test-suite/coqdoc/details.tex.out | 44 | ||||
| -rw-r--r-- | test-suite/coqdoc/details.v | 11 | ||||
| -rw-r--r-- | test-suite/micromega/bug_12790.v | 8 | ||||
| -rw-r--r-- | test-suite/micromega/bug_12791.v | 9 | ||||
| -rw-r--r-- | test-suite/ssr/noting_to_inject.v | 9 |
11 files changed, 283 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 0935617fbf..f7447d6cec 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -771,8 +771,6 @@ coq-makefile/%.log : coq-makefile/%/run.sh # coqdoc -coqdoc: $(patsubst %.sh,%.log,$(wildcard coqdoc/*.sh)) - $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ diff --git a/test-suite/bugs/closed/bug_12566_1.v b/test-suite/bugs/closed/bug_12566_1.v new file mode 100644 index 0000000000..22d95949bb --- /dev/null +++ b/test-suite/bugs/closed/bug_12566_1.v @@ -0,0 +1,16 @@ + +Class C (n:nat) := c{}. + +Instance c0 : C 0 := {}. + +Definition x := 0. + +Opaque x. + +Type _ : C x. +(* this is maybe wrong behaviour, if it changes just update the test *) + +Hint Opaque x : typeclass_instances. +Transparent x. + +Fail Type _ : C x. diff --git a/test-suite/coqdoc/bug12742.html.out b/test-suite/coqdoc/bug12742.html.out new file mode 100644 index 0000000000..75dd185ff9 --- /dev/null +++ b/test-suite/coqdoc/bug12742.html.out @@ -0,0 +1,67 @@ +<!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.bug12742</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.bug12742</h1> + +<div class="code"> +</div> + +<div class="doc"> +Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx + xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx. + Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx + xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx. Xxxxx xxxxx + xxxx xxxx xxx xxxxx xxxxxxxxxx: + +<div class="paragraph"> </div> + +<ul class="doclist"> +<li> <i>Xxxxxxxxx xxxxxxx xxxxxxx</i> xxxxxxx "xxxx-xxxxxx" xxxxxxxxx: + xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx <i>xxxx</i> xx + <i>xxxxx</i> (xx, xxxxxxxxx, <i>xxx'x xxxx: xxx xxx xx xxxx</i>). + Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx + xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx + xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx. Xxxxxxxx xx xxxx + xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx. + +<div class="paragraph"> </div> + + +</li> +<li> <i>Xxxxx xxxxxxxxxx</i> xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx + xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx + xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx. Xxxxxx xxxx xxxxx + xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx, + xxxxx xxxx xxxxxx. + +</li> +</ul> + +</div> +<div class="code"> +</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/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out new file mode 100644 index 0000000000..d7eba096fc --- /dev/null +++ b/test-suite/coqdoc/bug12742.tex.out @@ -0,0 +1,51 @@ +\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.bug12742}{Library }{Coqdoc.bug12742} + +\begin{coqdoccode} +\end{coqdoccode} +Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx + xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx. + Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx + xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx. Xxxxx xxxxx + xxxx xxxx xxx xxxxx xxxxxxxxxx: + + + +\begin{itemize} +\item \textit{Xxxxxxxxx xxxxxxx xxxxxxx} xxxxxxx ``xxxx-xxxxxx'' xxxxxxxxx: + xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx \textit{xxxx} xx + \textit{xxxxx} (xx, xxxxxxxxx, \textit{xxx'x xxxx: xxx xxx xx xxxx}). + Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx + xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx + xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx. Xxxxxxxx xx xxxx + xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx. + + + +\item \textit{Xxxxx xxxxxxxxxx} xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx + xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx + xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx. Xxxxxx xxxx xxxxx + xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx, + xxxxx xxxx xxxxxx. + +\end{itemize} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug12742.v b/test-suite/coqdoc/bug12742.v new file mode 100644 index 0000000000..8ce1faff00 --- /dev/null +++ b/test-suite/coqdoc/bug12742.v @@ -0,0 +1,20 @@ + (** Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx + xxxxxxxxxxxxxx: XX xxx xxxx xxxx xxxxxxxxx xxxxxxxxxxxxx xx xxxxx. + Xxx xx xxxxx xxx xxxx xxx xxxxxxxxxxx xx xxxxxxxx xxxxx xxx + xxxxxxx xxxxxxxxx xxxxxx xx xxxxxxx xxxxxxxxxxxx. Xxxxx xxxxx + xxxx xxxx xxx xxxxx xxxxxxxxxx: + + - _Xxxxxxxxx xxxxxxx xxxxxxx_ xxxxxxx "xxxx-xxxxxx" xxxxxxxxx: + xxx xxxx xxxx x xxxxxxxxxxx xxx xxxx xxxxxx xxxxxx _xxxx_ xx + _xxxxx_ (xx, xxxxxxxxx, _xxx'x xxxx: xxx xxx xx xxxx_). + Xxxxxxxx xxxxx xxxxxxxxxxxx xxx xxxxx xxxxxxx xx xxxxxxxx + xxxxxxx, xxxx xxxx xxxxxxx xxxxxxxxxxxx xx xxxxxx xxxxx xxx + xxx xxxx xxx xx x xxxxxxxxx xx xxxxxxxx. Xxxxxxxx xx xxxx + xxxxx xxxxxxx XXX xxxxxxx, XXX xxxxxxx, xxx xxxxx xxxxxxxx. + + - _Xxxxx xxxxxxxxxx_ xxx xxxxxx xxxxx xxxx xxxxxxxx xxx xxxx + xxxxxxx xxxxxxx xx xxxxxxxx xxxxxx xxxxx xxxxxxxxx xx xxxxx + xxxxxxxx xxx xxxx xxxxxxxxx xxxxxxx. Xxxxxx xxxx xxxxx + xxxxxxxxxx xxxxxxx Xxxxxxxx, Xxxx, Xxxxx, XXXx, XXX, xxx Xxx, + xxxxx xxxx xxxxxx. +*) diff --git a/test-suite/coqdoc/details.html.out b/test-suite/coqdoc/details.html.out new file mode 100644 index 0000000000..e1f1ad9867 --- /dev/null +++ b/test-suite/coqdoc/details.html.out @@ -0,0 +1,48 @@ +<!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.details</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.details</h1> + +<div class="code"> +</div> +<details><div class="code"> +<span class="id" title="keyword">Definition</span> <a id="foo" class="idref" href="#foo"><span class="id" title="definition">foo</span></a> : <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> := 3.<br/> +</div> +</details><div class="code"> + +<br/> +</div> +<details><summary>Foo bar </summary><div class="code"> +<span class="id" title="keyword">Fixpoint</span> <a id="idnat" class="idref" href="#idnat"><span class="id" title="definition">idnat</span></a> (<a id="x:1" class="idref" href="#x:1"><span class="id" title="binder">x</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#nat"><span class="id" title="inductive">nat</span></a> :=<br/> + <span class="id" title="keyword">match</span> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a> <span class="id" title="keyword">with</span><br/> + | <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/stdlib/Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Coqdoc.details.html#idnat:2"><span class="id" title="definition">idnat</span></a> <a class="idref" href="Coqdoc.details.html#x:1"><span class="id" title="variable">x</span></a>)<br/> + | 0 ⇒ 0<br/> + <span class="id" title="keyword">end</span>.<br/> +</div> +</details><div class="code"> +</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/details.tex.out b/test-suite/coqdoc/details.tex.out new file mode 100644 index 0000000000..37778944ba --- /dev/null +++ b/test-suite/coqdoc/details.tex.out @@ -0,0 +1,44 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.details}{Library }{Coqdoc.details} + +\begin{coqdoccode} +\end{coqdoccode} +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.details.foo}{foo}{\coqdocdefinition{foo}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} := 3.\coqdoceol +\end{coqdoccode} +\begin{coqdoccode} +\coqdocemptyline +\end{coqdoccode} +\begin{coqdoccode} +\coqdocnoindent +\coqdockw{Fixpoint} \coqdef{Coqdoc.details.idnat}{idnat}{\coqdocdefinition{idnat}} (\coqdef{Coqdoc.details.x:1}{x}{\coqdocbinder{x}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}) : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} :=\coqdoceol +\coqdocindent{1.00em} +\coqdockw{match} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}} \coqdockw{with}\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} \coqdocvar{x} \ensuremath{\Rightarrow} \coqexternalref{S}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{S}} (\coqref{Coqdoc.details.idnat:2}{\coqdocdefinition{idnat}} \coqref{Coqdoc.details.x:1}{\coqdocvariable{x}})\coqdoceol +\coqdocindent{1.00em} +\ensuremath{|} 0 \ensuremath{\Rightarrow} 0\coqdoceol +\coqdocindent{1.00em} +\coqdockw{end}.\coqdoceol +\end{coqdoccode} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/details.v b/test-suite/coqdoc/details.v new file mode 100644 index 0000000000..208e60317d --- /dev/null +++ b/test-suite/coqdoc/details.v @@ -0,0 +1,11 @@ +(* begin details *) +Definition foo : nat := 3. +(* end details *) + +(* begin details : Foo bar *) +Fixpoint idnat (x : nat) : nat := + match x with + | S x => S (idnat x) + | 0 => 0 + end. +(* end details *) diff --git a/test-suite/micromega/bug_12790.v b/test-suite/micromega/bug_12790.v new file mode 100644 index 0000000000..39d640ebd9 --- /dev/null +++ b/test-suite/micromega/bug_12790.v @@ -0,0 +1,8 @@ +Require Import Lia. + +Goal forall (a b c d x: nat), +S c = a - b -> x <= x + (S c) * d. +Proof. +intros a b c d x H. +lia. +Qed. diff --git a/test-suite/micromega/bug_12791.v b/test-suite/micromega/bug_12791.v new file mode 100644 index 0000000000..8aec1904a4 --- /dev/null +++ b/test-suite/micromega/bug_12791.v @@ -0,0 +1,9 @@ +Require Import Lia. + +Definition t := nat. + +Goal forall (a b: t), let c := a in b = a -> b = c. +Proof. + intros a b c H. + lia. +Qed. diff --git a/test-suite/ssr/noting_to_inject.v b/test-suite/ssr/noting_to_inject.v new file mode 100644 index 0000000000..95bbd3e777 --- /dev/null +++ b/test-suite/ssr/noting_to_inject.v @@ -0,0 +1,9 @@ +Require Import ssreflect ssrfun ssrbool. + + +Goal forall b : bool, b -> False. +Set Warnings "+spurious-ssr-injection". +Fail move=> b []. +Set Warnings "-spurious-ssr-injection". +move=> b []. +Abort. |