From b6733f0507e3e04fb6130b3f82a79e8835e1062f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 31 May 2017 00:30:00 +0200 Subject: Bump year in headers. --- test-suite/bench/lists-100.v | 2 +- test-suite/bench/lists_100.v | 2 +- test-suite/failure/Tauto.v | 2 +- test-suite/failure/clash_cons.v | 2 +- test-suite/failure/fixpoint1.v | 2 +- test-suite/failure/guard.v | 2 +- test-suite/failure/illtype1.v | 2 +- test-suite/failure/positivity.v | 2 +- test-suite/failure/redef.v | 2 +- test-suite/failure/search.v | 2 +- test-suite/ideal-features/Apply.v | 2 +- test-suite/misc/berardi_test.v | 2 +- test-suite/success/Check.v | 2 +- test-suite/success/Field.v | 2 +- test-suite/success/Tauto.v | 2 +- test-suite/success/TestRefine.v | 2 +- test-suite/success/eauto.v | 2 +- test-suite/success/eqdecide.v | 2 +- test-suite/success/extraction.v | 2 +- test-suite/success/inds_type_sec.v | 2 +- test-suite/success/induct.v | 2 +- test-suite/success/mutual_ind.v | 2 +- test-suite/success/unfold.v | 2 +- test-suite/typeclasses/NewSetoid.v | 2 +- 24 files changed, 24 insertions(+), 24 deletions(-) (limited to 'test-suite') diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v index 5c64716c72..eba1e01d72 100644 --- a/test-suite/bench/lists-100.v +++ b/test-suite/bench/lists-100.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Type := +| nilT : TupleT 0 +| consT {n} A : (A -> TupleT n) -> TupleT (S n). + +Inductive Tuple : forall n, TupleT n -> Type := + nil : Tuple _ nilT +| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F). + +Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type := + tmNil : TupleMap _ nilT nilT +| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n) + : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G). -- cgit v1.2.3 From 09cbae6c995c3e94ac8f0e53e6857da8e491a2fe Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 8 Jun 2017 14:54:39 +0200 Subject: Adding a test case as requested in bug 5205. --- test-suite/bugs/closed/5205.v | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 test-suite/bugs/closed/5205.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/5205.v b/test-suite/bugs/closed/5205.v new file mode 100644 index 0000000000..406f37a4b1 --- /dev/null +++ b/test-suite/bugs/closed/5205.v @@ -0,0 +1,6 @@ +Definition foo (n : nat) (m : nat) : nat := m. + +Arguments foo {_} _, _ _. + +Check foo 1 1. +Check foo (n:=1) 1. -- cgit v1.2.3 From 849bf3600fe11fea876c9aeea69fe806b0c8c5d8 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Fri, 9 Jun 2017 12:30:42 -0400 Subject: Fix Bug #5568, no dup notation warnings on repeated module imports --- test-suite/output/Notations.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'test-suite') diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 2ccca829d6..b9985a594f 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -1,3 +1,14 @@ +(* Bug 5568, don't warn for notations in repeated module import *) + +Module foo. +Notation compose := (fun g f => g f). +Notation "g & f" := (compose g f) (at level 10). +End foo. + +Import foo. +Import foo. +Import foo. + (**********************************************************************) (* Notations for if and let (submitted by Roland Zumkeller) *) -- cgit v1.2.3 From 5ddad92dfc81b0333990dc1956544e924a14600a Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Fri, 10 Mar 2017 12:00:35 -0500 Subject: Add tests for handling of warnings --- test-suite/output/RecognizePluginWarning.out | 0 test-suite/output/RecognizePluginWarning.v | 5 +++++ test-suite/output/UsePluginWarning.out | 1 + test-suite/output/UsePluginWarning.v | 7 +++++++ 4 files changed, 13 insertions(+) create mode 100644 test-suite/output/RecognizePluginWarning.out create mode 100644 test-suite/output/RecognizePluginWarning.v create mode 100644 test-suite/output/UsePluginWarning.out create mode 100644 test-suite/output/UsePluginWarning.v (limited to 'test-suite') diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out new file mode 100644 index 0000000000..e69de29bb2 diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v new file mode 100644 index 0000000000..cd667bbd00 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.v @@ -0,0 +1,5 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *) + +(* Test that mentioning a warning defined in plugins works. The failure +mode here is that these result in a warning about unknown warnings, since the +plugins are not known at command line parsing time. *) diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out new file mode 100644 index 0000000000..47409f3ec5 --- /dev/null +++ b/test-suite/output/UsePluginWarning.out @@ -0,0 +1 @@ +type foo = __ diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v new file mode 100644 index 0000000000..c6e0054641 --- /dev/null +++ b/test-suite/output/UsePluginWarning.v @@ -0,0 +1,7 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) + +Require Extraction. +Axiom foo : Prop. + +Extraction foo. + -- cgit v1.2.3