diff options
Diffstat (limited to 'test-suite')
52 files changed, 1030 insertions, 28 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_13249.v b/test-suite/bugs/closed/bug_13249.v new file mode 100644 index 0000000000..06f7ddbd3a --- /dev/null +++ b/test-suite/bugs/closed/bug_13249.v @@ -0,0 +1,9 @@ +Global Generalizable All Variables. + +Section test. + Context {A : Type}. + Context `{!foo A}. + + Goal foo A. + Proof. assumption. Defined. +End test. 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_13300.v b/test-suite/bugs/closed/bug_13300.v new file mode 100644 index 0000000000..e4fcd6dacc --- /dev/null +++ b/test-suite/bugs/closed/bug_13300.v @@ -0,0 +1,7 @@ +Polymorphic Definition type := Type. + +Inductive bad : type := . + +Fail Check bad : Prop. +Check bad : Set. +(* lowered as much as possible *) 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_13366.v b/test-suite/bugs/closed/bug_13366.v new file mode 100644 index 0000000000..06918a9266 --- /dev/null +++ b/test-suite/bugs/closed/bug_13366.v @@ -0,0 +1,5 @@ +Class Functor (F : Type -> Type) : Type := + fmap : F nat. + +Fail Definition blah := sum fmap. +(* used to be anomaly not an arity *) 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/bugs/closed/bug_9809.v b/test-suite/bugs/closed/bug_9809.v new file mode 100644 index 0000000000..4a7d2c7fac --- /dev/null +++ b/test-suite/bugs/closed/bug_9809.v @@ -0,0 +1,30 @@ +Section FreeMonad. + + Variable S : Type. + Variable P : S -> Type. + + Inductive FreeF A : Type := + | retFree : A -> FreeF A + | opr : forall s, (P s -> FreeF A) -> FreeF A. + +End FreeMonad. + +Section Fibonnacci. + + Inductive gen_op := call_op : nat -> gen_op. + Definition gen_ty (op : gen_op) := + match op with + | call_op _ => nat + end. + + Fail Definition fib0 (n:nat) : FreeF gen_op gen_ty nat := + match n with + | 0 + | 1 => retFree _ _ _ 1 + | S (S k) => + opr _ _ _ (call_op (S k)) + (fun r1 => opr _ _ _ (call_op k) + (fun r0 => retFree (* _ _ _ *) (r1 + r0))) + end. + +End Fibonnacci. diff --git a/test-suite/bugs/closed/bug_9971.v b/test-suite/bugs/closed/bug_9971.v new file mode 100644 index 0000000000..ef526dcd7d --- /dev/null +++ b/test-suite/bugs/closed/bug_9971.v @@ -0,0 +1,27 @@ +(* Test that it raises a normal error and not an anomaly *) +Set Primitive Projections. +Record prod A B := pair { fst : A ; snd : B }. +Arguments fst {A B} _. +Arguments snd {A B} _. +Arguments pair {A B} _ _. +Record piis := { dep_types : Type; indep_args : dep_types -> Type }. +Import EqNotations. +Goal forall (id : Set) (V : id) (piiio : id -> piis) + (Z : {ridc : id & prod (dep_types (piiio ridc)) True}) + (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}), + let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in + prod True (ida V (projT1 W)) -> + Z = existT _ V (pair (projT1 W) I) -> + ida (projT1 Z) (fst (projT2 Z)). + intros. + refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] + H in + let v := I in + _); + refine (snd X). + Undo. +Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))] + H in + let v := I in + snd X). +Abort. 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/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..a9bed49922 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -120,14 +120,14 @@ where letpair x [1] = {0}; return (1, 2, 3, 4) : nat * nat * nat * nat -{{ 1 | 1 // 1 }} - : nat -!!! _ _ : nat, True - : (nat -> Prop) * ((nat -> Prop) * Prop) ((*1).2).3 : nat *(1.2) : nat +{{ 1 | 1 // 1 }} + : nat +!!! _ _ : nat, True + : (nat -> Prop) * ((nat -> Prop) * Prop) ! '{{x, y}}, x.y = 0 : Prop exists x : nat, @@ -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..04a91c14d9 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -181,6 +181,13 @@ Notation "'letpair' x [1] = { a } ; 'return' ( b0 , b1 , .. , b2 )" := (let x:=a in ( .. (b0,b1) .., b2)). Check letpair x [1] = {0}; return (1,2,3,4). +(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) + +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Check (((id 1) + 2) + 3). +Check (id (1 + 2)). + (* Test spacing in #5569 *) Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) @@ -191,13 +198,6 @@ Check 1+1+1. Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). Check !!! (x y:nat), True. -(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) - -Notation "* x" := (id x) (only printing, at level 15, format "* x"). -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). -Check (((id 1) + 2) + 3). -Check (id (1 + 2)). - (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) (* for isolated "forall" (was not working already in 8.6) *) Notation "! x .. y , A" := (id (forall x, .. (id (forall y, A)) .. )) (at level 200, x binder). @@ -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/Notations4.out b/test-suite/output/Notations4.out index a6fd39c29b..86c4b3cccc 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -179,3 +179,21 @@ Found an inductive type while a pattern was expected. : Prop !!!! (nat, id), nat = true /\ id = false : Prop +∀ x : nat, x = 0 + : Prop +∀₁ x, x = 0 + : Prop +∀₁ x, x = 0 + : Prop +∀₂ x y, x + y = 0 + : Prop +((1, 2)) + : nat * nat +%% [x == 1] + : Prop +%%% [1] + : Prop +[[2]] + : nat * nat +%%% + : Type diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 0731819bba..6af192ea82 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -414,3 +414,76 @@ Module P. End NotationBinderNotMixedWithTerms. End P. + +Module MorePrecise1. + +(* A notation with limited iteration is strictly more precise than a + notation with unlimited iteration *) + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + +Check forall x, x = 0. + +Notation "∀₁ z , P" := (forall z, P) + (at level 200, right associativity) : type_scope. + +Check forall x, x = 0. + +Notation "∀₂ y x , P" := (forall y x, P) + (at level 200, right associativity) : type_scope. + +Check forall x, x = 0. +Check forall x y, x + y = 0. + +Notation "(( x , y ))" := (x,y) : core_scope. + +Check ((1,2)). + +End MorePrecise1. + +Module MorePrecise2. + +(* Case of a bound binder *) +Notation "%% [ x == y ]" := (forall x, S x = y) (at level 0, x pattern, y at level 60). + +(* Case of an internal binder *) +Notation "%%% [ y ]" := (forall x : nat, x = y) (at level 0). + +(* Check that the two previous notations are indeed finer *) +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'"). +Notation "∀' x .. y , P" := (forall y, .. (forall x, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀' x .. y ']' , '/' P ']'"). + +Check %% [x == 1]. +Check %%% [1]. + +Notation "[[ x ]]" := (pair 1 x). + +Notation "( x ; y ; .. ; z )" := (pair .. (pair x y) .. z). +Notation "[ x ; y ; .. ; z ]" := (pair .. (pair x z) .. y). + +(* Check which is finer *) +Check [[ 2 ]]. + +End MorePrecise2. + +Module MorePrecise3. + +(* This is about a binder not bound in a notation being strictly more + precise than a binder bound in the notation (since the notation + applies - a priori - stricly less often) *) + +Notation "%%%" := (forall x, x) (at level 0). + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'"). + +Check %%%. + +End MorePrecise3. 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/attributes.out b/test-suite/output/attributes.out new file mode 100644 index 0000000000..25572ee2aa --- /dev/null +++ b/test-suite/output/attributes.out @@ -0,0 +1,11 @@ +The command has indeed failed with message: +Attribute for canonical specified twice. +The command has indeed failed with message: +key 'polymorphic' has been already set. +The command has indeed failed with message: +Invalid value 'foo' for key polymorphic +use one of {yes, no} +The command has indeed failed with message: +Invalid syntax polymorphic(foo), try polymorphic={yes, no} instead. +The command has indeed failed with message: +Invalid syntax polymorphic(foo, bar), try polymorphic={yes, no} instead. diff --git a/test-suite/output/attributes.v b/test-suite/output/attributes.v new file mode 100644 index 0000000000..aef05e6cd4 --- /dev/null +++ b/test-suite/output/attributes.v @@ -0,0 +1,9 @@ +Fail #[canonical=yes, canonical=no] Definition a := 3. + +Fail #[universes(polymorphic=yes,polymorphic=no)] Definition a := 3. + +Fail #[universes(polymorphic=foo)] Definition a := 3. + +Fail #[universes(polymorphic(foo))] Definition a := 3. + +Fail #[universes(polymorphic(foo,bar))] Definition a := 3. diff --git a/test-suite/output/bug_10824.out b/test-suite/output/bug_10824.out new file mode 100644 index 0000000000..4bc5aafbca --- /dev/null +++ b/test-suite/output/bug_10824.out @@ -0,0 +1,4 @@ +!! + : Prop +!! + : Prop diff --git a/test-suite/output/bug_10824.v b/test-suite/output/bug_10824.v new file mode 100644 index 0000000000..01271f7d61 --- /dev/null +++ b/test-suite/output/bug_10824.v @@ -0,0 +1,12 @@ +Module A. +Notation F := False. +Notation "!!" := False (at level 100). +Check False. +End A. + +Module B. +Notation "!!" := False (at level 100). +Notation F := False. +Notation "!!" := False (at level 100). +Check False. +End B. 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/bug_7443.out b/test-suite/output/bug_7443.out new file mode 100644 index 0000000000..446ec6a1ad --- /dev/null +++ b/test-suite/output/bug_7443.out @@ -0,0 +1,13 @@ +Literal 1 + : Type +[1] + : Type +Literal 1 + : Type +[1] + : Type +The command has indeed failed with message: +The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". +Literal 1 + : Type diff --git a/test-suite/output/bug_7443.v b/test-suite/output/bug_7443.v new file mode 100644 index 0000000000..33f76dbcfa --- /dev/null +++ b/test-suite/output/bug_7443.v @@ -0,0 +1,37 @@ +Inductive type := nat | bool. +Definition denote (t : type) + := match t with + | nat => Datatypes.nat + | bool => Datatypes.bool + end. +Ltac reify t := + lazymatch eval cbv beta in t with + | Datatypes.nat => nat + | Datatypes.bool => bool + end. +Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing). +Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing). +Axiom Literal : forall {t}, denote t -> Type. +Declare Scope foo_scope. +Delimit Scope foo_scope with foo. +Open Scope foo_scope. +Section A. + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Literal 1 : Type *) (* as expected *) + Notation "[ x ]" := (Literal x) : foo_scope. + Check @Literal nat 1. (* Incorred: gives Literal 1 : Type when it should give [1]. Fixed by #12950 *) + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Incorrect: gives Literal 1 : Type when it should give [1]. This is disputable: + #12950 considers that giving an only parsing a previous both-parsing-and-printing notation *) +End A. +Section B. + Notation "[ x ]" := (Literal x) : foo_scope. + Check @Literal nat 1. (* [1] : Type *) + Fail Check [1]. (* As expected: The command has indeed failed with message: + The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". *) + Notation "[ x ]" := (Literal (t:=reify_type_of x) x) (only parsing) : foo_scope. + Check [1]. (* Should succeed, but instead fails with: Error: + The term "1" has type "Datatypes.nat" while it is expected to have type + "denote ?t". Fixed by #12950, but previous declaration is cancelled by #12950. *) +End B. diff --git a/test-suite/output/bug_9569.out b/test-suite/output/bug_9569.out new file mode 100644 index 0000000000..2d474e4933 --- /dev/null +++ b/test-suite/output/bug_9569.out @@ -0,0 +1,16 @@ +1 subgoal + + ============================ + exists I : True, I = Logic.I +1 subgoal + + ============================ + f True False True False (Logic.True /\ Logic.False) +1 subgoal + + ============================ + [I | I = Logic.I; I = Logic.I] = [I | I = Logic.I; I = Logic.I] +1 subgoal + + ============================ + [I & I = Logic.I | I = Logic.I; Logic.I = I] diff --git a/test-suite/output/bug_9569.v b/test-suite/output/bug_9569.v new file mode 100644 index 0000000000..ee5b052811 --- /dev/null +++ b/test-suite/output/bug_9569.v @@ -0,0 +1,18 @@ +Goal exists I, I = Logic.I. +Show. +Abort. + +Notation f x y p q r := ((forall x, p /\ r) /\ forall y, q /\ r). +Goal f True False True False (Logic.True /\ Logic.False). +Show. +Abort. + +Notation "[ x | y ; z ; .. ; t ]" := (pair .. (pair (forall x, y) (forall x, z)) .. (forall x, t)). +Goal [ I | I = Logic.I ; I = Logic.I ] = [ I | I = Logic.I ; I = Logic.I ]. +Show. +Abort. + +Notation "[ x & p | y ; .. ; z ; t ]" := (forall x, p -> y -> .. (forall x, p -> z -> forall x, p -> t) ..). +Goal [ I & I = Logic.I | I = Logic.I ; Logic.I = I ]. +Show. +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/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v index 4f8427dc5b..ea45fb3983 100644 --- a/test-suite/primitive/float/next_up_down.v +++ b/test-suite/primitive/float/next_up_down.v @@ -120,3 +120,46 @@ Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Pr Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)). Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)). Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)). + +Check (eq_refl : next_up nan = nan). +Check (eq_refl : next_down nan = nan). +Check (eq_refl : next_up neg_infinity = -0x1.fffffffffffffp+1023). +Check (eq_refl : next_down neg_infinity = neg_infinity). +Check (eq_refl : next_up (-0x1.fffffffffffffp+1023) = -0x1.ffffffffffffep+1023). +Check (eq_refl : next_down (-0x1.fffffffffffffp+1023) = neg_infinity). +Check (eq_refl : next_up (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffff9p+1023). +Check (eq_refl : next_down (-0x1.ffffffffffffap+1023) = -0x1.ffffffffffffbp+1023). +Check (eq_refl : next_up (-0x1.fffffffffffff) = -0x1.ffffffffffffe). +Check (eq_refl : next_down (-0x1.fffffffffffff) = -0x1p+1). +Check (eq_refl : next_up (-0x1p1) = -0x1.fffffffffffff). +Check (eq_refl : next_down (-0x1p1) = -0x1.0000000000001p+1). +Check (eq_refl : next_up (-0x1p-1022) = -0x0.fffffffffffffp-1022). +Check (eq_refl : next_down (-0x1p-1022) = -0x1.0000000000001p-1022). +Check (eq_refl : next_up (-0x0.fffffffffffffp-1022) = -0x0.ffffffffffffep-1022). +Check (eq_refl : next_down (-0x0.fffffffffffffp-1022) = -0x1p-1022). +Check (eq_refl : next_up (-0x0.01p-1022) = -0x0.00fffffffffffp-1022). +Check (eq_refl : next_down (-0x0.01p-1022) = -0x0.0100000000001p-1022). +Check (eq_refl : next_up (-0x0.0000000000001p-1022) = -0). +Check (eq_refl : next_down (-0x0.0000000000001p-1022) = -0x0.0000000000002p-1022). +Check (eq_refl : next_up (-0) = 0x0.0000000000001p-1022). +Check (eq_refl : next_down (-0) = -0x0.0000000000001p-1022). +Check (eq_refl : next_up 0 = 0x0.0000000000001p-1022). +Check (eq_refl : next_down 0 = -0x0.0000000000001p-1022). +Check (eq_refl : next_up 0x0.0000000000001p-1022 = 0x0.0000000000002p-1022). +Check (eq_refl : next_down 0x0.0000000000001p-1022 = 0). +Check (eq_refl : next_up 0x0.01p-1022 = 0x0.0100000000001p-1022). +Check (eq_refl : next_down 0x0.01p-1022 = 0x0.00fffffffffffp-1022). +Check (eq_refl : next_up 0x0.fffffffffffffp-1022 = 0x1p-1022). +Check (eq_refl : next_down 0x0.fffffffffffffp-1022 = 0x0.ffffffffffffep-1022). +Check (eq_refl : next_up 0x1p-1022 = 0x1.0000000000001p-1022). +Check (eq_refl : next_down 0x1p-1022 = 0x0.fffffffffffffp-1022). +Check (eq_refl : next_up 0x1p1 = 0x1.0000000000001p+1). +Check (eq_refl : next_down 0x1p1 = 0x1.fffffffffffff). +Check (eq_refl : next_up 0x1.fffffffffffff = 0x1p+1). +Check (eq_refl : next_down 0x1.fffffffffffff = 0x1.ffffffffffffe). +Check (eq_refl : next_up 0x1.ffffffffffffap+1023 = 0x1.ffffffffffffbp+1023). +Check (eq_refl : next_down 0x1.ffffffffffffap+1023 = 0x1.ffffffffffff9p+1023). +Check (eq_refl : next_up 0x1.fffffffffffffp+1023 = infinity). +Check (eq_refl : next_down 0x1.fffffffffffffp+1023 = 0x1.ffffffffffffep+1023). +Check (eq_refl : next_up infinity = infinity). +Check (eq_refl : next_down infinity = 0x1.fffffffffffffp+1023). 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/Template.v b/test-suite/success/Template.v index 656362b8fc..d11ae20b8d 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -37,7 +37,7 @@ Module Yes. End Yes. Module No. - #[universes(notemplate)] + #[universes(template=no)] Inductive Box (A:Type) : Type := box : A -> Box A. About Box. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index b403fc120c..b866c4b074 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -16,11 +16,16 @@ Definition ι T (x: T) := x. Check ι _ ι. +#[universes(polymorphic=no)] +Definition ιι T (x: T) := x. + +Fail Check ιι _ ιι. + #[program] Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. -#[program(true)] +#[program=yes] Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. @@ -43,3 +48,14 @@ Export Set Foo. Fail #[ export ] Export Foo. (* Attribute for Locality specified twice *) + +(* Tests for deprecated attribute syntax *) +Set Warnings "-deprecated-attribute-syntax". + +#[program(true)] +Fixpoint f (n: nat) {wf lt n} : nat := _. +Reset f. + +#[universes(monomorphic)] +Definition ιιι T (x: T) := x. +Fail Check ιιι _ ιιι. |