diff options
Diffstat (limited to 'test-suite')
71 files changed, 107 insertions, 78 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 552d007f85..a48a71c159 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -1,6 +1,6 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## ## <O___,, # (see CREDITS file for the list of authors) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## @@ -335,16 +335,16 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithm $(FAIL); \ fi; \ } > "$@" - @echo "CHECK $<" - $(HIDE){ \ - opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ + opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \ $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ - } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi stm: $(wildcard stm/*.v:%.v=%.v.log) $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @@ -362,15 +362,15 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v $(FAIL); \ fi; \ } > "$@" - @echo "CHECK $<" - $(HIDE){ \ + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ - } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" @@ -386,15 +386,15 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(FAIL); \ fi; \ } > "$@" - @echo "CHECK $<" - $(HIDE){ \ + @if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi + $(HIDE)if ! grep -q -F "Error!" $@; then { \ $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be checked (Error!)" ; \ $(FAIL); \ fi; \ - } > "$(shell dirname $<)/$(shell basename $< .v).chk.log" + } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" diff --git a/test-suite/bugs/closed/bug_10197.v b/test-suite/bugs/closed/bug_10197.v new file mode 100644 index 0000000000..920c5f5cb7 --- /dev/null +++ b/test-suite/bugs/closed/bug_10197.v @@ -0,0 +1,16 @@ +(* Some check about implicit arguments in fix *) + +Check fix f {f:nat} := match f with 0 => true | _ => false end. + +CoInductive stream := { this : nat ; next : option stream }. + +Check cofix f {f:nat} := {| this := f ; next := None |}. + +(* The following was ok from 8.4, just checking that the order is not + mixed up accidentally *) + +Check fix f (x : nat) (x : forall {a:nat}, a = 0 -> nat) := + match x eq_refl with 0 => true | _ => false end. + +Check fix f (x : forall {a:nat}, a = 0 -> bool) (x : nat) := + match x with 0 => true | _ => false end. diff --git a/test-suite/bugs/closed/bug_10225.v b/test-suite/bugs/closed/bug_10225.v new file mode 100644 index 0000000000..6d6bb39a65 --- /dev/null +++ b/test-suite/bugs/closed/bug_10225.v @@ -0,0 +1,7 @@ + +Class Bar := {}. +Instance bb : Bar := {}. + +Class Foo := { xx : Bar; foo : nat }. + +Fail Instance bar : Foo := { foo := 1 + 1; foo := 2 + 2 }. diff --git a/test-suite/bugs/closed/bug_3810.v b/test-suite/bugs/closed/bug_3810.v new file mode 100644 index 0000000000..0b2bef8a9b --- /dev/null +++ b/test-suite/bugs/closed/bug_3810.v @@ -0,0 +1,6 @@ +Class Foo. + +Fixpoint test (H : Foo) (n : nat) {A : Type} {struct n} : A. +Admitted. + +Check fun (x:Foo) => test x 0. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index c10cb0b869..6eef3c9845 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index 89299110be..88dee9a683 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index eb3d94526c..4b8e861616 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 2a5ad7789c..023a494a66 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index ec43ea5fc8..3988292248 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index 2798dcf974..ec8eb35b87 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index 981d14387d..b1a578d15c 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index 058c427c93..284acb88fc 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index 14eb1e3f96..5e1218851a 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v index 56ca24b6e2..4a840fe20c 100644 --- a/test-suite/output/ssr_explain_match.v +++ b/test-suite/output/ssr_explain_match.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index 6fc630056c..74f94a9bed 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/prerequisite/ssr_ssrsyntax1.v b/test-suite/prerequisite/ssr_ssrsyntax1.v index 2b404e2de0..1ffc83ecf8 100644 --- a/test-suite/prerequisite/ssr_ssrsyntax1.v +++ b/test-suite/prerequisite/ssr_ssrsyntax1.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/absevarprop.v b/test-suite/ssr/absevarprop.v index fa1de00957..d534443c32 100644 --- a/test-suite/ssr/absevarprop.v +++ b/test-suite/ssr/absevarprop.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/abstract_var2.v b/test-suite/ssr/abstract_var2.v index 7c57d2024f..aaeb80646b 100644 --- a/test-suite/ssr/abstract_var2.v +++ b/test-suite/ssr/abstract_var2.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/binders.v b/test-suite/ssr/binders.v index 97b7d830fa..a4b77257dc 100644 --- a/test-suite/ssr/binders.v +++ b/test-suite/ssr/binders.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/binders_of.v b/test-suite/ssr/binders_of.v index 69b52eacea..3f60a480dc 100644 --- a/test-suite/ssr/binders_of.v +++ b/test-suite/ssr/binders_of.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/caseview.v b/test-suite/ssr/caseview.v index 94b064b02f..098263ee4c 100644 --- a/test-suite/ssr/caseview.v +++ b/test-suite/ssr/caseview.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v index 7e60b04a6b..026f7538e8 100644 --- a/test-suite/ssr/congr.v +++ b/test-suite/ssr/congr.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/deferclear.v b/test-suite/ssr/deferclear.v index 85353dadff..817101a268 100644 --- a/test-suite/ssr/deferclear.v +++ b/test-suite/ssr/deferclear.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/dependent_type_err.v b/test-suite/ssr/dependent_type_err.v index a5789d8dd8..436813bc94 100644 --- a/test-suite/ssr/dependent_type_err.v +++ b/test-suite/ssr/dependent_type_err.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/derive_inversion.v b/test-suite/ssr/derive_inversion.v index abf63a20ce..a2c438f8fe 100644 --- a/test-suite/ssr/derive_inversion.v +++ b/test-suite/ssr/derive_inversion.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/elim.v b/test-suite/ssr/elim.v index 720f4f6607..15b1d91eef 100644 --- a/test-suite/ssr/elim.v +++ b/test-suite/ssr/elim.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/elim2.v b/test-suite/ssr/elim2.v index c7c20d8f8b..52fc2ed333 100644 --- a/test-suite/ssr/elim2.v +++ b/test-suite/ssr/elim2.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/elim_pattern.v b/test-suite/ssr/elim_pattern.v index ef4658287f..ecc5d1d5c7 100644 --- a/test-suite/ssr/elim_pattern.v +++ b/test-suite/ssr/elim_pattern.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/first_n.v b/test-suite/ssr/first_n.v index 4971add919..0d42a55390 100644 --- a/test-suite/ssr/first_n.v +++ b/test-suite/ssr/first_n.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/gen_have.v b/test-suite/ssr/gen_have.v index 249e006f9f..4adad3d3ac 100644 --- a/test-suite/ssr/gen_have.v +++ b/test-suite/ssr/gen_have.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/gen_pattern.v b/test-suite/ssr/gen_pattern.v index c0592e8843..0120d77194 100644 --- a/test-suite/ssr/gen_pattern.v +++ b/test-suite/ssr/gen_pattern.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/have_TC.v b/test-suite/ssr/have_TC.v index b3a26ed2c2..c74282ed4f 100644 --- a/test-suite/ssr/have_TC.v +++ b/test-suite/ssr/have_TC.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/have_transp.v b/test-suite/ssr/have_transp.v index 1c998da71b..d663780adc 100644 --- a/test-suite/ssr/have_transp.v +++ b/test-suite/ssr/have_transp.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/have_view_idiom.v b/test-suite/ssr/have_view_idiom.v index 3d6c9d9802..623eaac2b9 100644 --- a/test-suite/ssr/have_view_idiom.v +++ b/test-suite/ssr/have_view_idiom.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/havesuff.v b/test-suite/ssr/havesuff.v index aa1f71879e..3ca69bcc4c 100644 --- a/test-suite/ssr/havesuff.v +++ b/test-suite/ssr/havesuff.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/if_isnt.v b/test-suite/ssr/if_isnt.v index b8f6b77391..23bc581213 100644 --- a/test-suite/ssr/if_isnt.v +++ b/test-suite/ssr/if_isnt.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/intro_beta.v b/test-suite/ssr/intro_beta.v index 8a164bd809..dce4650611 100644 --- a/test-suite/ssr/intro_beta.v +++ b/test-suite/ssr/intro_beta.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/intro_noop.v b/test-suite/ssr/intro_noop.v index fdc85173a8..9e141a9487 100644 --- a/test-suite/ssr/intro_noop.v +++ b/test-suite/ssr/intro_noop.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/ipatalternation.v b/test-suite/ssr/ipatalternation.v index 6aa9a954c8..ae783ac7ed 100644 --- a/test-suite/ssr/ipatalternation.v +++ b/test-suite/ssr/ipatalternation.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/ltac_have.v b/test-suite/ssr/ltac_have.v index 380e52af40..3862aa72da 100644 --- a/test-suite/ssr/ltac_have.v +++ b/test-suite/ssr/ltac_have.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/ltac_in.v b/test-suite/ssr/ltac_in.v index bcdf96dded..e379c21773 100644 --- a/test-suite/ssr/ltac_in.v +++ b/test-suite/ssr/ltac_in.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/move_after.v b/test-suite/ssr/move_after.v index a7a9afea07..45c23e30c3 100644 --- a/test-suite/ssr/move_after.v +++ b/test-suite/ssr/move_after.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/multiview.v b/test-suite/ssr/multiview.v index f4e717b384..fcb7e2a520 100644 --- a/test-suite/ssr/multiview.v +++ b/test-suite/ssr/multiview.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/occarrow.v b/test-suite/ssr/occarrow.v index 49af7ae08a..8d11219a23 100644 --- a/test-suite/ssr/occarrow.v +++ b/test-suite/ssr/occarrow.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/patnoX.v b/test-suite/ssr/patnoX.v index d69f03ac3d..2dea5fcb6d 100644 --- a/test-suite/ssr/patnoX.v +++ b/test-suite/ssr/patnoX.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/pattern.v b/test-suite/ssr/pattern.v index 396f4f032c..ae4745b352 100644 --- a/test-suite/ssr/pattern.v +++ b/test-suite/ssr/pattern.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/primproj.v b/test-suite/ssr/primproj.v index cf61eb4363..89aa56e8ec 100644 --- a/test-suite/ssr/primproj.v +++ b/test-suite/ssr/primproj.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/rewpatterns.v b/test-suite/ssr/rewpatterns.v index f7993f402d..82d0112362 100644 --- a/test-suite/ssr/rewpatterns.v +++ b/test-suite/ssr/rewpatterns.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/set_lamda.v b/test-suite/ssr/set_lamda.v index a012ec680b..a18dde31bf 100644 --- a/test-suite/ssr/set_lamda.v +++ b/test-suite/ssr/set_lamda.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/set_pattern.v b/test-suite/ssr/set_pattern.v index 3ce75e879e..b513673215 100644 --- a/test-suite/ssr/set_pattern.v +++ b/test-suite/ssr/set_pattern.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/ssrsyntax2.v b/test-suite/ssr/ssrsyntax2.v index af839fabdb..c98ab98742 100644 --- a/test-suite/ssr/ssrsyntax2.v +++ b/test-suite/ssr/ssrsyntax2.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/tc.v b/test-suite/ssr/tc.v index ae4589ef30..bffb20d39b 100644 --- a/test-suite/ssr/tc.v +++ b/test-suite/ssr/tc.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/typeof.v b/test-suite/ssr/typeof.v index ca121fdb31..bd51230157 100644 --- a/test-suite/ssr/typeof.v +++ b/test-suite/ssr/typeof.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/unfold_Opaque.v b/test-suite/ssr/unfold_Opaque.v index 7c2b51de48..0b220b31f5 100644 --- a/test-suite/ssr/unfold_Opaque.v +++ b/test-suite/ssr/unfold_Opaque.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/unkeyed.v b/test-suite/ssr/unkeyed.v index 710941c307..eee1d1cf67 100644 --- a/test-suite/ssr/unkeyed.v +++ b/test-suite/ssr/unkeyed.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/view_case.v b/test-suite/ssr/view_case.v index 2721470c44..d212d377b6 100644 --- a/test-suite/ssr/view_case.v +++ b/test-suite/ssr/view_case.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/wlog_suff.v b/test-suite/ssr/wlog_suff.v index 43a8f3b8b7..3deceebb39 100644 --- a/test-suite/ssr/wlog_suff.v +++ b/test-suite/ssr/wlog_suff.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/wlogletin.v b/test-suite/ssr/wlogletin.v index 64e1ea84f7..2dca6d939f 100644 --- a/test-suite/ssr/wlogletin.v +++ b/test-suite/ssr/wlogletin.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/ssr/wlong_intro.v b/test-suite/ssr/wlong_intro.v index dd80f04359..c24b66f7b8 100644 --- a/test-suite/ssr/wlong_intro.v +++ b/test-suite/ssr/wlong_intro.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 36fecf7204..56a4fa0aad 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index fdf7797d4b..31e442549b 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index 7d01d3b07b..ea0cf43451 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index f1683078cb..287c77c866 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 5b616ccc33..28200f8783 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 9b3fb3c5c7..17c6a93d21 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 95ae070940..54c82ff6f1 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index 92fd6cb17d..ed781b3a40 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index da7df69e62..c8e5be93e9 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 2c76a13597..ac734de9df 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 72f0d94dea..b7ab75349e 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index 81c4a1469c..c5238eff22 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |