diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 2 | ||||
| -rw-r--r-- | test-suite/arithmetic/primitive.v | 12 | ||||
| -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/output/Notations4.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 8 | ||||
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 2 | ||||
| -rw-r--r-- | test-suite/success/primitive.v | 69 | ||||
| -rw-r--r-- | test-suite/success/sprop.v | 4 | ||||
| -rw-r--r-- | test-suite/success/unfold.v | 70 |
12 files changed, 309 insertions, 16 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/arithmetic/primitive.v b/test-suite/arithmetic/primitive.v deleted file mode 100644 index f62f6109e1..0000000000 --- a/test-suite/arithmetic/primitive.v +++ /dev/null @@ -1,12 +0,0 @@ -Section S. - Variable A : Type. - Fail Primitive int : let x := A in Set := #int63_type. - Fail Primitive add := #int63_add. -End S. - -(* [Primitive] should be forbidden in sections, otherwise its type after cooking -will be incorrect: - -Check int. - -*) 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/output/Notations4.out b/test-suite/output/Notations4.out index 9cb019ca56..fa03ec8193 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -119,3 +119,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) +File "stdin", line 297, characters 0-30: +Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] +0 :=: 0 + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b3270d4f92..90d8da2bec 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -290,3 +290,11 @@ Check V tt. Check fun x : nat => V x. End O. + +Module Bug12691. + +Notation "x :=: y" := True (at level 70, no associativity, only parsing). +Notation "x :=: y" := (x = y). +Check (0 :=: 0). + +End Bug12691. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index ba316ceb64..b8db52735d 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,7 +7,7 @@ bli : Type Axioms: bli : Type Axioms: -@seq relies on definitional UIP. +seq relies on definitional UIP. Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g diff --git a/test-suite/success/primitive.v b/test-suite/success/primitive.v new file mode 100644 index 0000000000..b2d02a0c49 --- /dev/null +++ b/test-suite/success/primitive.v @@ -0,0 +1,69 @@ +(* This file mostly tests for the error paths in declaring primitives. + Successes are tested in the various test-suite/primitive/* directories *) + +(* [Primitive] should be forbidden in sections, otherwise its type +after cooking will be incorrect. *) +Section S. + Variable A : Type. + Fail Primitive int : let x := A in Set := #int63_type. + Fail Primitive int := #int63_type. (* we fail even if section variable not used *) +End S. +Section S. + Fail Primitive int := #int63_type. (* we fail even if no section variables *) +End S. + +(* can't declare primitives with nonsense types *) +Fail Primitive xx : nat := #int63_type. + +(* non-cumulative conversion *) +Fail Primitive xx : Type := #int63_type. + +(* check evars *) +Fail Primitive xx : let x := _ in Set := #int63_type. + +(* explicit type is unified with expected type, not just converted + + extra universes are OK for monomorphic primitives (even though + their usefulness is questionable, there's no difference compared + with predeclaring them) + *) +Primitive xx : let x := Type in _ := #int63_type. + +(* double declaration *) +Fail Primitive yy := #int63_type. + +Module DoubleCarry. + (* XXX maybe should be an output test: this is the case where the new + declaration is already in the nametab so can be nicely printed *) + Module M. + Variant carry (A : Type) := + | C0 : A -> carry A + | C1 : A -> carry A. + + Register carry as kernel.ind_carry. + End M. + + Module N. + Variant carry (A : Type) := + | C0 : A -> carry A + | C1 : A -> carry A. + + Fail Register carry as kernel.ind_carry. + End N. +End DoubleCarry. + +(* univ polymorphic primitives *) + +(* universe count must be as expected *) +Fail Primitive array@{u v} : Type@{u} -> Type@{v} := #array_type. + +(* use a phantom universe to ensure we check conversion not just the universe count *) +Fail Primitive array@{u} : Set -> Set := #array_type. + +(* no constraints allowed! *) +Fail Primitive array@{u | Set < u} : Type@{u} -> Type@{u} := #array_type. + +(* unification works for polymorphic primitives too (although universe + counts mean it's not enough) *) +Fail Primitive array : let x := Type in _ -> Type := #array_type. +Primitive array : _ -> Type := #array_type. diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v index d3e2749088..3a6dfb1e11 100644 --- a/test-suite/success/sprop.v +++ b/test-suite/success/sprop.v @@ -171,6 +171,10 @@ End sFix. Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0. +(* Check that VM/native properly keep the relevance of the predicate in the case info + (bad-relevance warning as error otherwise) *) +Definition vm_rebuild_case := Eval vm_compute in eq_sind. + Require Import ssreflect. Goal forall T : SProp, T -> True. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 7af09585d0..712cb6a135 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -15,6 +15,7 @@ Goal EQ nat 0 0. Hint Unfold EQ. auto. Qed. +End toto. (* Check regular failure when statically existing ref does not exist any longer at run time *) @@ -23,4 +24,71 @@ Goal let x := 0 in True. intro x. Fail (clear x; unfold x). Abort. -End toto. + +(* Static analysis of unfold *) + +Module A. + +Opaque id. +Ltac f := unfold id. +Goal id 0 = 0. +Fail f. +Transparent id. +f. +Abort. + +End A. + +Module B. + +Module Type T. Axiom n : nat. End T. + +Module F(X:T). +Ltac f := unfold X.n. +End F. + +Module M. Definition n := 0. End M. +Module N := F M. +Goal match M.n with 0 => 0 | S _ => 1 end = 0. +N.f. +match goal with |- 0=0 => idtac end. +Abort. + +End B. + +Module C. + +(* We reject inductive types and constructors *) + +Fail Ltac g := unfold nat. +Fail Ltac g := unfold S. + +End C. + +Module D. + +(* In interactive mode, we delay the interpretation of short names *) + +Notation x := Nat.add. + +Goal let x := 0 in x = 0+0. +unfold x. +match goal with |- 0 = 0 => idtac end. +Abort. + +Goal let x := 0 in x = 0+0. +intro; unfold x. (* dynamic binding (but is it really the most natural?) *) +match goal with |- 0 = 0+0 => idtac end. +Abort. + +Goal let fst := 0 in fst = Datatypes.fst (0,0). +unfold fst. +match goal with |- 0 = 0 => idtac end. +Abort. + +Goal let fst := 0 in fst = Datatypes.fst (0,0). +intro; unfold fst. (* dynamic binding *) +match goal with |- 0 = Datatypes.fst (0,0) => idtac end. +Abort. + +End D. |