diff options
Diffstat (limited to 'test-suite')
46 files changed, 791 insertions, 16 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_12348.v b/test-suite/bugs/closed/bug_12348.v new file mode 100644 index 0000000000..93ba6f17e0 --- /dev/null +++ b/test-suite/bugs/closed/bug_12348.v @@ -0,0 +1,11 @@ +(* Was raising an anomaly before 8.13 *) +Check let 'tt := tt in + let X := nat in + let b : bool := _ in + (fun n : nat => 0 : X) : _. + +(* Was raising an ill-typed instance error before 8.13 *) +Check let 'tt := tt in + let X := nat in + let b : bool := true in + (fun n : nat => 0 : X) : _. diff --git a/test-suite/bugs/closed/bug_13246.v b/test-suite/bugs/closed/bug_13246.v new file mode 100644 index 0000000000..11f5baaaf4 --- /dev/null +++ b/test-suite/bugs/closed/bug_13246.v @@ -0,0 +1,69 @@ +Axiom _0: Prop. + +From Coq Require Export Morphisms Setoid Utf8. + +Class Equiv A := equiv: relation A. + +Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity). +Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity). +Reserved Notation "■ P" (at level 20, right associativity). + +(** Define the scope *) +Declare Scope bi_scope. +Delimit Scope bi_scope with I. + +Structure bi := + Bi { bi_car :> Type; + bi_entails : bi_car → bi_car → Prop; + bi_impl : bi_car → bi_car → bi_car; + bi_forall : ∀ A, (A → bi_car) → bi_car; }. + +Declare Instance bi_equiv `{PROP:bi} : Equiv (bi_car PROP). + +Arguments bi_car : simpl never. +Arguments bi_entails {PROP} _%I _%I : simpl never, rename. +Arguments bi_impl {PROP} _%I _%I : simpl never, rename. +Arguments bi_forall {PROP _} _%I : simpl never, rename. + +Notation "P ⊢ Q" := (bi_entails P%I Q%I) . +Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) . + +Infix "→" := bi_impl : bi_scope. +Notation "∀ x .. y , P" := + (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope. + +(* bug disappears if definitional class *) +Class Plainly (PROP : bi) := { plainly : PROP -> PROP; }. +Notation "■ P" := (plainly P) : bi_scope. + +Section S. + Context {I : Type} {PROP : bi} `(Plainly PROP). + + Lemma plainly_forall `{Plainly PROP} {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊣⊢ ■ (∀ a, Ψ a). + Proof. Admitted. + + Global Instance entails_proper : + Proper (equiv ==> equiv ==> iff) (bi_entails : relation PROP). + Proof. Admitted. + + Global Instance impl_proper : + Proper (equiv ==> equiv ==> equiv) (@bi_impl PROP). + Proof. Admitted. + + Global Instance forall_proper A : + Proper (pointwise_relation _ equiv ==> equiv) (@bi_forall PROP A). + Proof. Admitted. + + Declare Instance PROP_Equivalence: Equivalence (@equiv PROP _). + + Set Mangle Names. + Lemma foo (P : I -> PROP) K: + K ⊢ ∀ (j : I) + (_ : Prop) (* bug disappears if this is removed *) + , (∀ i0, ■ P i0) → P j. + Proof. + setoid_rewrite plainly_forall. + (* retype in case the tactic did some nonsense *) + match goal with |- ?T => let _ := type of T in idtac end. + Abort. +End S. diff --git a/test-suite/bugs/closed/bug_13278.v b/test-suite/bugs/closed/bug_13278.v new file mode 100644 index 0000000000..9831a4d205 --- /dev/null +++ b/test-suite/bugs/closed/bug_13278.v @@ -0,0 +1,15 @@ +Inductive even: nat -> Prop := +| evenB: even 0 +| evenS: forall n, even n -> even (S (S n)). + +Goal even 1 -> False. +Proof. + refine (fun a => match a with end). +Qed. + +Goal even 1 -> False. +Proof. + refine (fun a => match a in even n + return match n with 1 => False | _ => True end : Prop + with evenB => I | evenS _ _ => I end). +Qed. diff --git a/test-suite/bugs/closed/bug_13330.v b/test-suite/bugs/closed/bug_13330.v new file mode 100644 index 0000000000..d13de2e58d --- /dev/null +++ b/test-suite/bugs/closed/bug_13330.v @@ -0,0 +1,17 @@ +Polymorphic Inductive path {A : Type} (x : A) : A -> Type := + refl : path x x. + +Goal False. +Proof. +simple refine (let H : False := _ in _). ++ exact_no_check I. ++ assert (path true false -> path false true). + (** Create a dummy polymorphic side-effect *) + { + intro IHn. + rewrite IHn. + reflexivity. + } + exact H. +Fail Qed. +Abort. 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/bugs/closed/bug_13363.v b/test-suite/bugs/closed/bug_13363.v new file mode 100644 index 0000000000..cc11aa93b6 --- /dev/null +++ b/test-suite/bugs/closed/bug_13363.v @@ -0,0 +1,17 @@ +Axiom X : Type. +Axiom P : (X -> unit) -> Prop. + +Axiom F: unit -> unit. +Axiom G : unit -> unit. + +Lemma Hyp ss': + P (fun y : X => ss') -> + P (fun y : X => G (F ss')). +Admitted. + +Lemma bug : exists x, P x. +Proof. +intros. +eexists (fun y : X => G _). +eapply Hyp. cbn beta. +Abort. diff --git a/test-suite/bugs/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v index 462a615d91..f3a19c2b89 100644 --- a/test-suite/bugs/closed/bug_3513.v +++ b/test-suite/bugs/closed/bug_3513.v @@ -13,7 +13,7 @@ Infix "|--" := lentails (at level 79, no associativity). Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. Infix "-|-" := lequiv (at level 85, no associativity). -Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit. Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. Section ILogic_Fun. Context (T: Type) `{TType: type T}. diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v index d667022e68..2d4d7d02cc 100644 --- a/test-suite/bugs/closed/bug_4095.v +++ b/test-suite/bugs/closed/bug_4095.v @@ -15,7 +15,7 @@ Infix "|--" := lentails (at level 79, no associativity). Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. Infix "-|-" := lequiv (at level 85, no associativity). -Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit. Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. Section ILogic_Fun. Context (T: Type) `{TType: type T}. diff --git a/test-suite/bugs/closed/bug_5512.v b/test-suite/bugs/closed/bug_5512.v new file mode 100644 index 0000000000..f885e31352 --- /dev/null +++ b/test-suite/bugs/closed/bug_5512.v @@ -0,0 +1,10 @@ +(* Check that an anomaly is not raised *) +(* It should however eventually succeed... *) +Goal exists x, x. +Proof. +simple refine (ex_intro _ _ _). +shelve. +(* The failure is due to Type(u)<=Prop for u an arbitrary sort + variable being rejected *) +Fail simple refine (_ _). +Abort. diff --git a/test-suite/bugs/closed/bug_6042.v b/test-suite/bugs/closed/bug_6042.v new file mode 100644 index 0000000000..72f612560b --- /dev/null +++ b/test-suite/bugs/closed/bug_6042.v @@ -0,0 +1,7 @@ +Class C (n: nat) := T{x:True}. +Generalizable All Variables. + +Fail Instance i : C n. + +Instance i : `(C n). +Proof. repeat constructor. Defined. 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/misc/13330.sh b/test-suite/misc/13330.sh new file mode 100755 index 0000000000..7340559432 --- /dev/null +++ b/test-suite/misc/13330.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +$coqc misc/13330/bug_13330.v +R=$? + +if [ $R == 0 ]; then + exit 1 +else + exit 0 +fi diff --git a/test-suite/misc/13330/bug_13330.v b/test-suite/misc/13330/bug_13330.v new file mode 100644 index 0000000000..acf6e80c48 --- /dev/null +++ b/test-suite/misc/13330/bug_13330.v @@ -0,0 +1,16 @@ +Polymorphic Inductive path {A : Type} (x : A) : A -> Type := + refl : path x x. + +Goal False. +Proof. +simple refine (let H : False := _ in _). ++ exact_no_check I. ++ assert (path true false -> path false true). + (** Create a dummy polymorphic side-effect *) + { + intro IHn. + rewrite IHn. + reflexivity. + } + exact H. +Qed. diff --git a/test-suite/output/HintLocality.out b/test-suite/output/HintLocality.out new file mode 100644 index 0000000000..37a0613b25 --- /dev/null +++ b/test-suite/output/HintLocality.out @@ -0,0 +1,92 @@ +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +The command has indeed failed with message: +This command does not support the global attribute in sections. +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all except: id +Cut: _ +For any goal -> +For nat -> +For S (modes !) -> + +Non-discriminated database +Unfoldable variable definitions: all +Unfoldable constant definitions: all +Cut: emp +For any goal -> +For nat -> simple apply 0 ; trivial(level 1, pattern nat, id 0) + diff --git a/test-suite/output/HintLocality.v b/test-suite/output/HintLocality.v new file mode 100644 index 0000000000..4481335907 --- /dev/null +++ b/test-suite/output/HintLocality.v @@ -0,0 +1,72 @@ +(** Test hint command locality w.r.t. modules *) + +Create HintDb foodb. +Create HintDb bardb. +Create HintDb quxdb. + +#[global] Hint Immediate O : foodb. +#[global] Hint Immediate O : bardb. +#[global] Hint Immediate O : quxdb. + +Module Test. + +#[global] Hint Cut [ _ ] : foodb. +#[global] Hint Mode S ! : foodb. +#[global] Hint Opaque id : foodb. +#[global] Remove Hints O : foodb. + +#[local] Hint Cut [ _ ] : bardb. +#[local] Hint Mode S ! : bardb. +#[local] Hint Opaque id : bardb. +#[local] Remove Hints O : bardb. + +#[export] Hint Cut [ _ ] : quxdb. +#[export] Hint Mode S ! : quxdb. +#[export] Hint Opaque id : quxdb. +#[export] Remove Hints O : quxdb. + +(** All three agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +End Test. + +(** bardb and quxdb agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +Import Test. + +(** foodb and quxdb agree here *) + +Print HintDb foodb. +Print HintDb bardb. +Print HintDb quxdb. + +(** Test hint command locality w.r.t. sections *) + +Create HintDb secdb. + +#[global] Hint Immediate O : secdb. + +Section Sec. + +Fail #[global] Hint Cut [ _ ] : secdb. +Fail #[global] Hint Mode S ! : secdb. +Fail #[global] Hint Opaque id : secdb. +Fail #[global] Remove Hints O : secdb. + +#[local] Hint Cut [ _ ] : secdb. +#[local] Hint Mode S ! : secdb. +#[local] Hint Opaque id : secdb. +#[local] Remove Hints O : secdb. + +Print HintDb secdb. + +End Sec. + +Print HintDb secdb. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index bd22d45059..623ca316c9 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -249,3 +249,5 @@ myfoo01 tt : nat myfoo01 tt : nat +1 ⪯ 2 ⪯ 3 ⪯ 4 + : Prop diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 839df99ea7..ce97d909a7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -410,3 +410,13 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) End Issue8126. + +Module RecursiveNotationPartialApp. + +(* Discussed on Coq Club, 28 July 2020 *) +Notation "x ⪯ y ⪯ .. ⪯ z ⪯ t" := + ((fun b A a => a <= b /\ A b) y .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) .. x) + (at level 70, y at next level, z at next level, t at next level). +Check 1 ⪯ 2 ⪯ 3 ⪯ 4. + +End RecursiveNotationPartialApp. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index ef4c6bac93..0f5fd91d93 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -462,3 +462,7 @@ inr: forall {A B : Type}, B -> A + B inl: forall {A B : Type}, A -> A + B (use "About" for full details on the implicit arguments of inl and inr) f: None = 0 +partition_cons1: + forall [A : Type] (f : A -> bool) (a : A) (l : list A) [l1 l2 : list A], + partition f l = (l1, l2) -> + f a = true -> partition f (a :: l) = (a :: l1, l2) diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v index 2f29e1aff1..3419d5ac62 100644 --- a/test-suite/output/Search.v +++ b/test-suite/output/Search.v @@ -96,3 +96,9 @@ Module WithCoercions. Axiom f : None = 0. Search (None = 0). End WithCoercions. + +Require Import List. + +Module Wish13349. +Search partition "1" inside List. +End Wish13349. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 70427220ed..3f07261ca6 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -7,3 +7,5 @@ H is already used. The command has indeed failed with message: H is already used. a +The command has indeed failed with message: +This variable is used in hypothesis H. diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v index 96b6d652c9..8526e43a23 100644 --- a/test-suite/output/Tactics.v +++ b/test-suite/output/Tactics.v @@ -30,3 +30,11 @@ Goal True. assert_succeeds should_not_loop. assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *) Abort. + +Module IntroWildcard. + +Theorem foo : { p:nat*nat & p = (0,0) } -> True. +Fail intros ((n,_),H). +Abort. + +End IntroWildcard. diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v index 2e4008ae56..0bd3d5fa40 100644 --- a/test-suite/output/TypeclassDebug.v +++ b/test-suite/output/TypeclassDebug.v @@ -2,6 +2,7 @@ Parameter foo : Prop. Axiom H : foo -> foo. +#[global] Hint Resolve H : foo. Goal foo. Typeclasses eauto := debug. diff --git a/test-suite/output/UnboundRef.out b/test-suite/output/UnboundRef.out new file mode 100644 index 0000000000..a574e97e0f --- /dev/null +++ b/test-suite/output/UnboundRef.out @@ -0,0 +1,3 @@ +File "stdin", line 1, characters 11-12: +Error: The reference a was not found in the current environment. + diff --git a/test-suite/output/UnboundRef.v b/test-suite/output/UnboundRef.v new file mode 100644 index 0000000000..fd08ae0c5c --- /dev/null +++ b/test-suite/output/UnboundRef.v @@ -0,0 +1,2 @@ +Check Prop a b. +(* Prop is because we need a real head for the application *) 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/output/locate.out b/test-suite/output/locate.out index 93d9d6cf7b..0196ead5e4 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,2 +1,8 @@ Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) Notation "x && y" := (andb x y) : bool_scope +Notation "'U' t" := (S t) (default interpretation) +Notation "'_' t" := (S t) (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation) diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v index af8b0ee193..6995743531 100644 --- a/test-suite/output/locate.v +++ b/test-suite/output/locate.v @@ -1,3 +1,26 @@ Set Printing Width 400. Notation "b1 && b2" := (if b1 then b2 else false). Locate "&&". + +Module M. + +Notation "'U' t" := (S t) (at level 0). +Notation "'_' t" := (S t) (at level 0). +Locate "U". (* was wrongly returning also "'_' t" *) +Locate "_". + +End M. + +Module N. + +(* Was not working at some time *) +Locate "( t , u , .. , v )". + +(* Was working though *) +Locate "( _ , _ , .. , _ )". + +(* We also support this *) +Locate "( t , u )". +Locate "( t , u , v )". + +End N. diff --git a/test-suite/report.sh b/test-suite/report.sh index 5b74bee0c7..0b8497b809 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -21,7 +21,7 @@ cp summary.log "$SAVEDIR"/ rm "$FAILED" # print info -if [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then +if [ -n "$CI" ] || [ -n "$PRINT_LOGS" ]; then find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do printf '%s\n' "$file" cat "$file" diff --git a/test-suite/ssr/ipat_apply.v b/test-suite/ssr/ipat_apply.v new file mode 100644 index 0000000000..2f7986aea6 --- /dev/null +++ b/test-suite/ssr/ipat_apply.v @@ -0,0 +1,13 @@ +Require Import ssreflect. + +Section Apply. + +Variable P : nat -> Prop. +Lemma test_apply A B : forall (f : A -> B) (a : A), B. + +Proof. +move=> /[apply] b. +exact. +Qed. + +End Apply. diff --git a/test-suite/ssr/ipat_dup.v b/test-suite/ssr/ipat_dup.v new file mode 100644 index 0000000000..b1936df31d --- /dev/null +++ b/test-suite/ssr/ipat_dup.v @@ -0,0 +1,13 @@ +Require Import ssreflect. + +Section Dup. + +Variable P : nat -> Prop. + +Lemma test_dup1 : forall n : nat, P n. +Proof. move=> /[dup] m n; suff: P n by []. Abort. + +Lemma test_dup2 : let n := 1 in False. +Proof. move=> /[dup] m n; have : m = n := eq_refl. Abort. + +End Dup. diff --git a/test-suite/ssr/ipat_swap.v b/test-suite/ssr/ipat_swap.v new file mode 100644 index 0000000000..1d78a2a009 --- /dev/null +++ b/test-suite/ssr/ipat_swap.v @@ -0,0 +1,13 @@ +Require Import ssreflect. + +Section Swap. + +Definition P n := match n with 1 => true | _ => false end. + +Lemma test_swap1 : forall (n : nat) (b : bool), P n = b. +Proof. move=> /[swap] b n; suff: P n = b by []. Abort. + +Lemma test_swap1 : let n := 1 in let b := true in False. +Proof. move=> /[swap] b n; have : P n = b := eq_refl. Abort. + +End Swap. diff --git a/test-suite/success/CumulInd.v b/test-suite/success/CumulInd.v new file mode 100644 index 0000000000..f24d13b8af --- /dev/null +++ b/test-suite/success/CumulInd.v @@ -0,0 +1,20 @@ + +(* variances other than Invariant are forbidden for non-cumul inductives *) +Fail Inductive foo@{+u} : Prop := . +Fail Polymorphic Inductive foo@{*u} : Prop := . +Inductive foo@{=u} : Prop := . + +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. + +Inductive force_invariant@{=u} : Prop := . +Fail Definition lift@{u v | u < v} (x:force_invariant@{u}) : force_invariant@{v} := x. + +Inductive force_covariant@{+u} : Prop := . +Fail Definition lift@{u v | v < u} (x:force_covariant@{u}) : force_covariant@{v} := x. +Definition lift@{u v | u < v} (x:force_covariant@{u}) : force_covariant@{v} := x. + +Fail Inductive not_irrelevant@{*u} : Prop := nirr (_ : Type@{u}). +Inductive check_covariant@{+u} : Prop := cov (_ : Type@{u}). + +Fail Inductive not_covariant@{+u} : Prop := ncov (_ : Type@{u} -> nat). diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 382c252727..fb8bbfd043 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -51,8 +51,8 @@ Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ Notation c3 x := ((@pair') _ x). Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *) Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *) -Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *) -Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end. +Check c3 0 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with c3 0 y 0 => 2 | _ => 1 end. (* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) (* unless an atomic @ is given *) diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 06697af901..8b7d239dcd 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -26,3 +26,15 @@ Definition c := ε : U. Goal True. assert (nat * nat). Abort. + +(* Check propagation of scopes in indirect applications to references *) + +Module PropagateIndirect. +Notation "0" := true : bool_scope. + +Axiom f : bool -> bool -> nat. +Check (@f 0) 0. + +Record R := { p : bool -> nat }. +Check fun r => r.(@p) 0. +End PropagateIndirect. 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. |