aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-01-21 16:45:23 +0100
committerPierre-Marie Pédrot2016-01-21 16:45:23 +0100
commitbe0eca32fae93ed4793c2f839bb9e725b6a963d1 (patch)
treec2c5dce5ce24f5a2a8cade9e69410599c00e2b55 /test-suite
parent9c2662eecc398f38be3b6280a8f760cc439bc31c (diff)
parent5e23fb90b39dfa014ae5c4fb46eb713cca09dbff (diff)
Merge branch 'v8.5'
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bench/lists-100.v2
-rw-r--r--test-suite/bench/lists_100.v2
-rw-r--r--test-suite/bugs/closed/4420.v19
-rw-r--r--test-suite/failure/Tauto.v2
-rw-r--r--test-suite/failure/clash_cons.v2
-rw-r--r--test-suite/failure/fixpoint1.v2
-rw-r--r--test-suite/failure/guard.v2
-rw-r--r--test-suite/failure/illtype1.v2
-rw-r--r--test-suite/failure/positivity.v2
-rw-r--r--test-suite/failure/redef.v2
-rw-r--r--test-suite/failure/search.v2
-rw-r--r--test-suite/ideal-features/Apply.v2
-rw-r--r--test-suite/misc/berardi_test.v2
-rw-r--r--test-suite/success/Check.v2
-rw-r--r--test-suite/success/Field.v2
-rw-r--r--test-suite/success/Tauto.v2
-rw-r--r--test-suite/success/TestRefine.v2
-rw-r--r--test-suite/success/eauto.v2
-rw-r--r--test-suite/success/eqdecide.v2
-rw-r--r--test-suite/success/extraction.v2
-rw-r--r--test-suite/success/inds_type_sec.v2
-rw-r--r--test-suite/success/induct.v2
-rw-r--r--test-suite/success/mutual_ind.v2
-rw-r--r--test-suite/success/unfold.v2
-rw-r--r--test-suite/typeclasses/NewSetoid.v2
25 files changed, 43 insertions, 24 deletions
diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v
index 352c7cea74..5c64716c72 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v
index 352c7cea74..5c64716c72 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 *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/bugs/closed/4420.v b/test-suite/bugs/closed/4420.v
new file mode 100644
index 0000000000..0e16cb2399
--- /dev/null
+++ b/test-suite/bugs/closed/4420.v
@@ -0,0 +1,19 @@
+Module foo.
+ Context (Char : Type).
+ Axiom foo : Type -> Type.
+ Goal foo Char = foo Char.
+ change foo with (fun x => foo x).
+ cbv beta.
+ reflexivity.
+ Defined.
+End foo.
+
+Inductive foo (A : Type) : Prop := I. (*Top.1*)
+Lemma bar : foo Type. (*Top.3*)
+Proof.
+ Set Printing Universes.
+change foo with (fun x : Type => foo x). (*Top.4*)
+cbv beta.
+apply I. (* I Type@{Top.3} : (fun x : Type@{Top.4} => foo x) Type@{Top.3} *)
+Defined.
+
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index 749db00027..d91d159d9c 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
index 8e34ffbdab..b3fbff680b 100644
--- a/test-suite/failure/clash_cons.v
+++ b/test-suite/failure/clash_cons.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v
index 7b52316ed1..c2b521c214 100644
--- a/test-suite/failure/fixpoint1.v
+++ b/test-suite/failure/fixpoint1.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index b3a0a33562..8db2785837 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v
index 7e4c5ac57b..8ed3af1ce4 100644
--- a/test-suite/failure/illtype1.v
+++ b/test-suite/failure/illtype1.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v
index 30762a77f3..8089de2bf0 100644
--- a/test-suite/failure/positivity.v
+++ b/test-suite/failure/positivity.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v
index e5db81768a..c8dc6303f7 100644
--- a/test-suite/failure/redef.v
+++ b/test-suite/failure/redef.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v
index a6e6bc4891..648ab0820c 100644
--- a/test-suite/failure/search.v
+++ b/test-suite/failure/search.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v
index ed46eb2298..c8e9af216e 100644
--- a/test-suite/ideal-features/Apply.v
+++ b/test-suite/ideal-features/Apply.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v
index 219686b959..a64db4dab7 100644
--- a/test-suite/misc/berardi_test.v
+++ b/test-suite/misc/berardi_test.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 87c38cfa06..e4ee351c3a 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index 8db08b6d78..438e461357 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 01d9afb426..767f15be72 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 3090f40cde..c8a8b862fa 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 9e57801e06..773dd321eb 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 1b5c7f183e..1f6af0dc44 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 57f3775d7e..0086e090bd 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index b733aef6db..c729b23ce7 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 9413b8dae9..1ed731f50f 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index 54cfa658c8..45c1a5e584 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 2954e25562..d595cbc2b8 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v
index 6f37de6583..49f20a23f5 100644
--- a/test-suite/typeclasses/NewSetoid.v
+++ b/test-suite/typeclasses/NewSetoid.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 18:08:02 +0000