diff options
Diffstat (limited to 'test-suite')
36 files changed, 201 insertions, 153 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 16a56f4408..8239600b1d 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -1,10 +1,12 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & CNRS-Universite Paris Diderot # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## # This is a standalone Makefile to run the test-suite. It can be used # outside of the Coq source tree (if BIN is overridden). diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v deleted file mode 100644 index 64a93aeb00..0000000000 --- a/test-suite/bugs/closed/2850.v +++ /dev/null @@ -1,2 +0,0 @@ -Definition id {A} (x : A) := x. -Fail Compute id. diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index c3c97d3f59..0d347b262d 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -1,5 +1,4 @@ Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. Module A. Import Coq.Lists.List Coq.Vectors.Vector. @@ -21,12 +20,10 @@ Delimit Scope mylist_scope with mylist. Bind Scope mylist_scope with mylist. Arguments mynil {_}, _. Arguments mycons {_} _ _. -Notation " [] " := mynil (compat "8.5") : mylist_scope. Notation " [ ] " := mynil (format "[ ]") : mylist_scope. Notation " [ x ] " := (mycons x nil) : mylist_scope. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. -Import Coq.Compat.Coq85. Locate Module VectorNotations. Import VectorDef.VectorNotations. @@ -35,11 +32,3 @@ Check []%mylist : mylist _. Check [ ]%mylist : mylist _. Check [ ]%list : list _. End A. - -Module B. -Import Coq.Compat.Coq85. - -Goal True. - idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) -Abort. -End B. diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v deleted file mode 100644 index bbb34f465c..0000000000 --- a/test-suite/bugs/closed/4785_compat_85.v +++ /dev/null @@ -1,46 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.5") -*- *) -Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. - -Module A. -Import Coq.Lists.List Coq.Vectors.Vector. -Import ListNotations. -Check [ ]%list : list _. -Import VectorNotations ListNotations. -Delimit Scope vector_scope with vector. -Check [ ]%vector : Vector.t _ _. -Check []%vector : Vector.t _ _. -Check [ ]%list : list _. -Fail Check []%list : list _. - -Goal True. - idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *) -Abort. - -Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). -Delimit Scope mylist_scope with mylist. -Bind Scope mylist_scope with mylist. -Arguments mynil {_}, _. -Arguments mycons {_} _ _. -Notation " [] " := mynil (compat "8.5") : mylist_scope. -Notation " [ ] " := mynil (format "[ ]") : mylist_scope. -Notation " [ x ] " := (mycons x nil) : mylist_scope. -Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. - -Import Coq.Compat.Coq85. -Locate Module VectorNotations. -Import VectorDef.VectorNotations. - -Check []%vector : Vector.t _ _. -Check []%mylist : mylist _. -Check [ ]%mylist : mylist _. -Check [ ]%list : list _. -End A. - -Module B. -Import Coq.Compat.Coq85. - -Goal True. - idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) -Abort. -End B. diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v index dbc3d46fce..6f2bcb9685 100644 --- a/test-suite/bugs/closed/4798.v +++ b/test-suite/bugs/closed/4798.v @@ -1,3 +1,3 @@ Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "8.4"). +Notation "|" := 1 (compat "8.6"). Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v index 3be36d8475..39299883ad 100644 --- a/test-suite/bugs/closed/4873.v +++ b/test-suite/bugs/closed/4873.v @@ -1,6 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. -Require Import Coq.Compat.Coq85. Fixpoint tuple' T n : Type := match n with diff --git a/test-suite/bugs/closed/6878.v b/test-suite/bugs/closed/6878.v new file mode 100644 index 0000000000..70f1b3127a --- /dev/null +++ b/test-suite/bugs/closed/6878.v @@ -0,0 +1,8 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo : Prop. +End T. + +(** Used to anomaly *) +Fail Module M : T with Definition foo := Type. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 19976b41bd..81d5b6358e 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**** Tactics Tauto and Intuition ****) diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index 1761cc437d..89299110be 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Teste la verification d'unicite des noms de constr *) diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index 0739982442..eb3d94526c 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Fail Fixpoint PreParadox (u : unit) : False := PreParadox u. (*Definition Paradox := PreParadox tt.*) diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 312dc48bea..2a5ad7789c 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Fixpoint F (n:nat) : False := F (match F n with end). diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index fdd1bddd88..ec43ea5fc8 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,8 +1,10 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Fail Check (S S). diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index b21204b9e4..2798dcf974 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Negative occurrence *) diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index c49dbd7cae..981d14387d 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Definition toto := Set. Fail Definition toto := Set. diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index fae6cd6f3b..058c427c93 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Fail SearchPattern (_ = _) outside n_existe_pas. diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index 85680e94b9..14eb1e3f96 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* This needs step by step unfolding *) diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out new file mode 100644 index 0000000000..0904d5540b --- /dev/null +++ b/test-suite/output/Load.out @@ -0,0 +1,6 @@ +f = 2 + : nat +u = I + : True +The command has indeed failed with message: +Files processed by Load cannot leave open proofs. diff --git a/test-suite/output/Load.v b/test-suite/output/Load.v new file mode 100644 index 0000000000..967507415a --- /dev/null +++ b/test-suite/output/Load.v @@ -0,0 +1,7 @@ +Load "output/load/Load_noproof.v". +Print f. + +Load "output/load/Load_proof.v". +Print u. + +Fail Load "output/load/Load_openproof.v". diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v index 08918981a4..a498db3e89 100644 --- a/test-suite/output/PrintInfos.v +++ b/test-suite/output/PrintInfos.v @@ -26,6 +26,7 @@ About bar. Print bar. About Peano. (* Module *) +Set Warnings "-deprecated". About existS2. (* Notation *) Arguments eq_refl {A} {x}, {A} x. diff --git a/test-suite/output/load/Load_noproof.v b/test-suite/output/load/Load_noproof.v new file mode 100644 index 0000000000..aaf1ffe26d --- /dev/null +++ b/test-suite/output/load/Load_noproof.v @@ -0,0 +1 @@ +Definition f := 2. diff --git a/test-suite/output/load/Load_openproof.v b/test-suite/output/load/Load_openproof.v new file mode 100644 index 0000000000..204d4ecbfe --- /dev/null +++ b/test-suite/output/load/Load_openproof.v @@ -0,0 +1 @@ +Lemma k : True. diff --git a/test-suite/output/load/Load_proof.v b/test-suite/output/load/Load_proof.v new file mode 100644 index 0000000000..e47f66a193 --- /dev/null +++ b/test-suite/output/load/Load_proof.v @@ -0,0 +1,2 @@ +Lemma u : True. +Proof. exact I. Qed. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 82b51b1ffb..36fecf7204 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Compiling the theories allows testing parsing and typing but not printing *) (* This file tests that pretty-printing does not fail *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 018b22c489..fdf7797d4b 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**** Tests of Field with real numbers ****) diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index bffd96044d..7d01d3b07b 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**** Tactics Tauto and Intuition ****) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 87296744c4..f1683078cb 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (************************************************************************) diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 9b0ff1c8fe..c44747379f 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Class A (A : Type). diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 055434df01..9b3fb3c5c7 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Inductive T : Set := diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 83726bfdc5..95ae070940 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Require Coq.extraction.Extraction. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index 7e9095dfd7..92fd6cb17d 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) Section S. Inductive T (U : Type) : Type := diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 35d7929877..da7df69e62 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Test des definitions inductives imbriquees *) diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index c4c5623897..2c76a13597 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Definition mutuellement inductive et dependante *) diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 62249666b3..448d0082db 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -151,10 +151,25 @@ Abort. (* Check that rewriting within evars still work (was broken in 8.5beta1) *) - Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y. intros; eexists; eexists. rewrite H. Undo. subst. Abort. + +(* Check that iterated rewriting does not rewrite in the side conditions *) +(* Example from Sigurd Schneider, extracted from contrib containers *) + +Lemma EQ + : forall (e e' : nat), True -> e = e'. +Admitted. + +Lemma test (v1 v2 v3: nat) (v' : v1 = v2) : v2 = v1. +Proof. + rewrite <- (EQ v1 v2) in *. + exact v'. + (* There should be only two side conditions *) + exact I. + exact I. +Qed. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index ce1c33fc40..de8aa252b8 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Test le Hint Unfold sur des var locales *) diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v new file mode 100644 index 0000000000..2c8b099ef0 --- /dev/null +++ b/test-suite/success/vm_evars.v @@ -0,0 +1,23 @@ +Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) := +match n with +| 0 => x +| S n => iter n f (f x) +end. + +Goal nat -> True. +Proof. +intros n. +evar (f : nat -> nat). +cut (iter 10 f 0 = 0). +vm_compute. +intros; constructor. +instantiate (f := (fun x => x)). +reflexivity. +Qed. + +Goal exists x, x = 5 + 5. +Proof. + eexists. + vm_compute. + reflexivity. +Qed. diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index 37d197a15c..81c4a1469c 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Certified Haskell Prelude. |