diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_11816.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13348.v | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13354.v | 10 | ||||
| -rw-r--r-- | test-suite/coqdoc/binder.tex.out | 3 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug12742.tex.out | 1 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.html.out | 6 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.tex.out | 8 | ||||
| -rw-r--r-- | test-suite/coqdoc/bug5700.v | 2 | ||||
| -rw-r--r-- | test-suite/coqdoc/links.tex.out | 4 | ||||
| -rw-r--r-- | test-suite/coqdoc/verbatim.html.out | 114 | ||||
| -rw-r--r-- | test-suite/coqdoc/verbatim.tex.out | 84 | ||||
| -rw-r--r-- | test-suite/coqdoc/verbatim.v | 40 | ||||
| -rw-r--r-- | test-suite/output/bug_13266.out | 12 | ||||
| -rw-r--r-- | test-suite/output/bug_13266.v | 18 | ||||
| -rw-r--r-- | test-suite/success/proof_using_noinit.v | 9 |
15 files changed, 312 insertions, 11 deletions
diff --git a/test-suite/bugs/closed/bug_11816.v b/test-suite/bugs/closed/bug_11816.v new file mode 100644 index 0000000000..82a317b250 --- /dev/null +++ b/test-suite/bugs/closed/bug_11816.v @@ -0,0 +1,2 @@ +(* This should be an error, not an anomaly *) +Fail Definition foo := fix foo (n : nat) { wf n n } := 0. diff --git a/test-suite/bugs/closed/bug_13348.v b/test-suite/bugs/closed/bug_13348.v new file mode 100644 index 0000000000..d3d5d3e5b4 --- /dev/null +++ b/test-suite/bugs/closed/bug_13348.v @@ -0,0 +1,10 @@ +Generalizable All Variables. + +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. +Arguments populate {_} _. + +Set Mangle Names. +Axioms _0 _1 _2 : Prop. + +Instance impl_inhabited {A} {B} {_3:Inhabited B} : Inhabited (A -> B) + := populate (fun _ => inhabitant). diff --git a/test-suite/bugs/closed/bug_13354.v b/test-suite/bugs/closed/bug_13354.v new file mode 100644 index 0000000000..fbda10a9d2 --- /dev/null +++ b/test-suite/bugs/closed/bug_13354.v @@ -0,0 +1,10 @@ + +Primitive array := #array_type. + +Definition testArray : array nat := [| 1; 2; 4 | 0 : nat |]. + +Definition on_array {A:Type} (x:array A) : Prop := True. + +Check on_array testArray. + +Check @on_array nat testArray. diff --git a/test-suite/coqdoc/binder.tex.out b/test-suite/coqdoc/binder.tex.out index 2b5648aee6..aceccc25fd 100644 --- a/test-suite/coqdoc/binder.tex.out +++ b/test-suite/coqdoc/binder.tex.out @@ -20,7 +20,8 @@ \begin{coqdoccode} \end{coqdoccode} -Link binders \begin{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 diff --git a/test-suite/coqdoc/bug12742.tex.out b/test-suite/coqdoc/bug12742.tex.out index d7eba096fc..a8f4c254cb 100644 --- a/test-suite/coqdoc/bug12742.tex.out +++ b/test-suite/coqdoc/bug12742.tex.out @@ -46,6 +46,7 @@ Xxx xxxx xx xxxxx xxxxxxx xxxxx xxx xxxxxxxx xxxxxxx xxx xxx xxxx xxxxx xxxx xxxxxx. \end{itemize} + \begin{coqdoccode} \end{coqdoccode} \end{document} diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index 286e8bba4d..84214a73d3 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -22,8 +22,7 @@ </div> <div class="doc"> -<pre>foo (* bar *) </pre> - +<code> foo (* {bar_bar} *) </code> </div> <div class="code"> <span class="id" title="keyword">Definition</span> <a id="const1" class="idref" href="#const1"><span class="id" title="definition">const1</span></a> := 1.<br/> @@ -32,8 +31,7 @@ </div> <div class="doc"> -<pre>more (* nested (* comments *) within verbatim *) </pre> - +<code> more (* nested (* comments *) within verbatim *) </code> </div> <div class="code"> <span class="id" title="keyword">Definition</span> <a id="const2" class="idref" href="#const2"><span class="id" title="definition">const2</span></a> := 2.<br/> diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out index 1a1af5dfdd..f2b12f0079 100644 --- a/test-suite/coqdoc/bug5700.tex.out +++ b/test-suite/coqdoc/bug5700.tex.out @@ -20,14 +20,14 @@ \begin{coqdoccode} \end{coqdoccode} -\begin{verbatim}foo (* bar *) \end{verbatim} - \begin{coqdoccode} +\texttt{ foo (* \{bar\_bar\} *) } +\begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol \coqdocemptyline \end{coqdoccode} -\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim} - \begin{coqdoccode} +\texttt{ more (* nested (* comments *) within verbatim *) } +\begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol \end{coqdoccode} diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v index 839034a48f..fc985276af 100644 --- a/test-suite/coqdoc/bug5700.v +++ b/test-suite/coqdoc/bug5700.v @@ -1,4 +1,4 @@ -(** << foo (* bar *) >> *) +(** << foo (* {bar_bar} *) >> *) Definition const1 := 1. (** << more (* nested (* comments *) within verbatim *) >> *) diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out index 2304f5ecc1..412a9ca6ac 100644 --- a/test-suite/coqdoc/links.tex.out +++ b/test-suite/coqdoc/links.tex.out @@ -36,6 +36,7 @@ Various checks for coqdoc \item ``..'' should be rendered correctly \end{itemize} + \begin{coqdoccode} \coqdocemptyline \coqdocnoindent @@ -166,7 +167,8 @@ skip skip - skip \begin{coqdoccode} + skip +\begin{coqdoccode} \coqdocemptyline \end{coqdoccode} \end{document} diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out new file mode 100644 index 0000000000..bf9f975ee8 --- /dev/null +++ b/test-suite/coqdoc/verbatim.html.out @@ -0,0 +1,114 @@ +<!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.verbatim</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library Coqdoc.verbatim</h1> + +<div class="code"> +</div> + +<div class="doc"> + +<div class="paragraph"> </div> + +<pre> +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +</pre> + +<div class="paragraph"> </div> + +This line and the following shows <code>verbatim </code> text: + +<div class="paragraph"> </div> + +<code> A stand-alone inline verbatim </code> + +<div class="paragraph"> </div> + +<code> A non-ended inline verbatim to test line location +</code> + +<div class="paragraph"> </div> + +<ul class="doclist"> +<li> item 1 + +</li> +<li> item 2 is <code>verbatim</code> + +</li> +<li> item 3 is <code>verbatim</code> too +<br/> +<span class="inlinecode"><span class="id" title="var">A</span> <span class="id" title="var">coq</span> <span class="id" title="var">block</span> : <span class="id" title="keyword">∀</span> <span class="id" title="var">n</span>, <span class="id" title="var">n</span> = 0 +<div class="paragraph"> </div> + +</span> +</li> +<li> <code>verbatim</code> again, and a formula <span class="inlinecode"></span> <span class="inlinecode"><span class="id" title="var">True</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">False</span></span> <span class="inlinecode"></span> + +</li> +<li> +<pre> +multiline +verbatim +</pre> + +</li> +<li> last item + +</li> +</ul> + +<div class="paragraph"> </div> + +<center><table class="infrule"> +<tr class="infruleassumption"> + <td class="infrule">Γ ⊢ A</td> + <td class="infrulenamecol" rowspan="3"> + + </td></tr> +<tr class="infrulemiddle"> + <td class="infrule"><hr /></td> +</tr> +<tr class="infruleassumption"> + <td class="infrule">Γ ⊢ A ∨ B</td> + <td></td> +</td> +</table></center> +<div class="paragraph"> </div> + +<pre> +A non-ended block verbatim to test line location + +*) +</pre> +</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/verbatim.tex.out b/test-suite/coqdoc/verbatim.tex.out new file mode 100644 index 0000000000..b692f6ad6a --- /dev/null +++ b/test-suite/coqdoc/verbatim.tex.out @@ -0,0 +1,84 @@ +\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.verbatim}{Library }{Coqdoc.verbatim} + +\begin{coqdoccode} +\end{coqdoccode} + + +\begin{verbatim} +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +\end{verbatim} + + +This line and the following shows \texttt{verbatim } text: + + +\texttt{ A stand-alone inline verbatim } + + +\texttt{ A non-ended inline verbatim to test line location +} + + + +\begin{itemize} +\item item 1 + +\item item 2 is \texttt{verbatim} + +\item item 3 is \texttt{verbatim} too +\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdocvar{A} \coqdocvar{coq} \coqdocvar{block} : \coqdockw{\ensuremath{\forall}} \coqdocvar{n}, \coqdocvar{n} = 0 + +\coqdocemptyline + +\item \texttt{verbatim} again, and a formula \coqdocvar{True} \ensuremath{\rightarrow} \coqdocvar{False} + +\item +\begin{verbatim} +multiline +verbatim +\end{verbatim} + +\item last item + +\end{itemize} + + +\begin{verbatim} +Γ ⊢ A +---- +Γ ⊢ A ∨ B +\end{verbatim} + + +\begin{verbatim} +A non-ended block verbatim to test line location + +*) +\end{verbatim} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/verbatim.v b/test-suite/coqdoc/verbatim.v new file mode 100644 index 0000000000..129a5117c9 --- /dev/null +++ b/test-suite/coqdoc/verbatim.v @@ -0,0 +1,40 @@ +(** + +<< +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +>> + +This line and the following shows << verbatim >> text: + +<< A stand-alone inline verbatim >> + +<< A non-ended inline verbatim to test line location + + +- item 1 +- item 2 is <<verbatim>> +- item 3 is <<verbatim>> too +[[ +A coq block : forall n, n = 0 +]] +- <<verbatim>> again, and a formula [ True -> False ] +- +<< +multiline +verbatim +>> +- last item + +[[[ +Γ ⊢ A +---- +Γ ⊢ A ∨ B +]]] + +<< +A non-ended block verbatim to test line location + +*) diff --git a/test-suite/output/bug_13266.out b/test-suite/output/bug_13266.out new file mode 100644 index 0000000000..034830f1ac --- /dev/null +++ b/test-suite/output/bug_13266.out @@ -0,0 +1,12 @@ +The command has indeed failed with message: +Abstracting over the terms "S", "p" and "u" leads to a term +fun (S0 : Type) (p0 : proc S0) (_ : S0) => p0 = Tick -> True +which is ill-typed. +Reason is: Illegal application: +The term "@eq" of type "forall A : Type, A -> A -> Prop" +cannot be applied to the terms + "proc S0" : "Prop" + "p0" : "proc S0" + "Tick" : "proc unit" +The 3rd term has type "proc unit" which should be coercible to +"proc S0". diff --git a/test-suite/output/bug_13266.v b/test-suite/output/bug_13266.v new file mode 100644 index 0000000000..e59455a326 --- /dev/null +++ b/test-suite/output/bug_13266.v @@ -0,0 +1,18 @@ +Inductive proc : Type -> Type := +| Tick : proc unit +. + +Inductive exec : + forall T, proc T -> T -> Prop := +| ExecTick : + exec _ (Tick) tt +. + +Lemma foo : + exec _ Tick tt -> + True. +Proof. + intros H. + remember Tick as p. + Fail induction H. +Abort. diff --git a/test-suite/success/proof_using_noinit.v b/test-suite/success/proof_using_noinit.v new file mode 100644 index 0000000000..f99b49619c --- /dev/null +++ b/test-suite/success/proof_using_noinit.v @@ -0,0 +1,9 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) + +Section A. +Variable A : Prop. +Hypothesis a : A. +Lemma b : A. +Proof using a. +Admitted. +End A. |