diff options
Diffstat (limited to 'test-suite')
121 files changed, 747 insertions, 122 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 94011447d7..c0bdb29fab 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 ## @@ -97,7 +97,7 @@ COMPLEXITY := $(if $(bogomips),complexity) BUGS := bugs/opened bugs/closed INTERACTIVE := interactive UNIT_TESTS := unit-tests -VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ +VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \ output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \ coqdoc ssr arithmetic ltac2 @@ -164,6 +164,7 @@ summary: $(call summary_dir, "Failure tests", failure); \ $(call summary_dir, "Bugs tests", bugs); \ $(call summary_dir, "Output tests", output); \ + $(call summary_dir, "Output tests with coqtop", output-coqtop); \ $(call summary_dir, "Output (modulo time changes) tests", output-modulo-time); \ $(call summary_dir, "Interactive tests", interactive); \ $(call summary_dir, "Micromega tests", micromega); \ @@ -299,6 +300,11 @@ unit-tests/%.ml.log: unit-tests/%.ml unit-tests/src/$(UNIT_LINK) $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.toplevel,oUnit \ -I unit-tests/src $(UNIT_LINK) $< -o $<.test; $(HIDE)./$<.test +unit-tests/ide/%.ml.log: unit-tests/ide/%.ml unit-tests/src/$(UNIT_LINK) + $(SHOW) 'TEST $<' + $(HIDE)$(OCAMLBEST) -linkall -linkpkg -package coq.ide,oUnit \ + -I unit-tests/src $(UNIT_LINK) $< -o $<.test; + $(HIDE)./$<.test ####################################################################### # Other generic tests @@ -335,16 +341,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 +368,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 +392,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,"$<")" @@ -420,8 +426,32 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) fi; \ } > "$@" +$(addsuffix .log,$(wildcard output-coqtop/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) + @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" + $(HIDE){ \ + echo $(call log_intro,$<); \ + output=$*.out.real; \ + $(coqtop) < "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + | grep -v "Welcome to Coq" \ + | grep -v "\[Loading ML file" \ + | grep -v "Skipping rcfile loading" \ + | grep -v "^<W>" \ + | sed 's/File "[^"]*"/File "stdin"/' \ + > $$output; \ + diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ + if [ $$R = 0 ]; then \ + echo $(log_success); \ + echo " $<...Ok"; \ + rm $$output; \ + else \ + echo $(log_failure); \ + echo " $<...Error! (unexpected output)"; \ + $(FAIL); \ + fi; \ + } > "$@" + .PHONY: approve-output -approve-output: output +approve-output: output output-coqtop $(HIDE)for f in output/*.out.real; do \ mv "$$f" "$${f%.real}"; \ echo "Updated $${f%.real}!"; \ @@ -561,7 +591,6 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) export coqc="$(coqc)"; \ export coqtop="$(coqc)"; \ export coqdep="$(coqdep)"; \ - export coqtopbyte="$(coqtopbyte)"; \ "$<" 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ diff --git a/test-suite/README.md b/test-suite/README.md index e81da0830f..a2d5905710 100644 --- a/test-suite/README.md +++ b/test-suite/README.md @@ -76,7 +76,9 @@ The error "(bug seems to be opened, please check)" when running compile. There are also output tests in [`output`](output) which consist of a `.v` file -and a `.out` file with the expected output. +and a `.out` file with the expected output. Output tests in this directory are +run with coqc in -test-mode. Output tests in [`output-coqtop`](output-coqtop) +work the same way, but are run with coqtop. There are unit tests of OCaml code in [`unit-tests`](unit-tests). These tests are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as diff --git a/test-suite/bugs/closed/bug_10161.v b/test-suite/bugs/closed/bug_10161.v new file mode 100644 index 0000000000..3d262b89fe --- /dev/null +++ b/test-suite/bugs/closed/bug_10161.v @@ -0,0 +1,8 @@ +Inductive SwitchT (A : Type) : Type := +| switchT : forall T, SwitchT T -> SwitchT A. + +Set Printing Universes. + +Fail Inductive UseSwitchT := +| useSwitchT : SwitchT UseSwitchT -> UseSwitchT. +(* used to stack overflow, should be univ inconsistency cannot satisfy u = u+1 *) 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_10264.v b/test-suite/bugs/closed/bug_10264.v new file mode 100644 index 0000000000..8351f8325b --- /dev/null +++ b/test-suite/bugs/closed/bug_10264.v @@ -0,0 +1,10 @@ +Require Import Program.Tactics. + +Definition bla (A:Type) := A. +Existing Class bla. + +Program Instance fubar : bla nat := {}. +Next Obligation. +Fail exact bool. +exact 0. +Qed. diff --git a/test-suite/bugs/closed/bug_1618.v b/test-suite/bugs/closed/bug_1618.v index a7be12e26f..041055a38f 100644 --- a/test-suite/bugs/closed/bug_1618.v +++ b/test-suite/bugs/closed/bug_1618.v @@ -20,3 +20,4 @@ a := match a return (P a) with | A1 n => f n end. +Proof. Defined. diff --git a/test-suite/bugs/closed/bug_2137.v b/test-suite/bugs/closed/bug_2137.v index b1f54b1766..981cc94dc1 100644 --- a/test-suite/bugs/closed/bug_2137.v +++ b/test-suite/bugs/closed/bug_2137.v @@ -3,7 +3,7 @@ The fsetdec tactic is sensitive to which way round the arguments to <> are. In the small, self-contained example below, it is able to solve the goal if it knows that "b <> a", but not if it knows that "a <> b". I would expect -it to be able to solve hte goal in either case. +it to be able to solve the goal in either case. I have coq r12238. diff --git a/test-suite/bugs/closed/bug_2603.v b/test-suite/bugs/closed/bug_2603.v index 371bfdc575..64c656a7a6 100644 --- a/test-suite/bugs/closed/bug_2603.v +++ b/test-suite/bugs/closed/bug_2603.v @@ -3,7 +3,7 @@ As noticed by A. Appel in bug #2603, module names and definition names used to be in the same namespace. But conflict with names of constructors (or 2nd mutual inductive...) used to not be checked -enough, leading to stange situations. +enough, leading to strange situations. - In 8.3pl3 we introduced checks that forbid uniformly the following situations. diff --git a/test-suite/bugs/closed/bug_3080.v b/test-suite/bugs/closed/bug_3080.v index 36ab7ff599..06719653fe 100644 --- a/test-suite/bugs/closed/bug_3080.v +++ b/test-suite/bugs/closed/bug_3080.v @@ -15,4 +15,4 @@ Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : function_scope. Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *) -Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *) +Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arguments to [compose] *) 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/bugs/closed/bug_4306.v b/test-suite/bugs/closed/bug_4306.v index 80c348d207..f1bce04451 100644 --- a/test-suite/bugs/closed/bug_4306.v +++ b/test-suite/bugs/closed/bug_4306.v @@ -30,3 +30,5 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) | Gt => y :: foo (xs, ys') end end. +Proof. +Defined. diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v index 5162f352df..26731e3292 100644 --- a/test-suite/bugs/closed/bug_4503.v +++ b/test-suite/bugs/closed/bug_4503.v @@ -29,7 +29,7 @@ End ILogic. Set Printing Universes. -(* There is stil a problem if the class is universe polymorphic *) +(* There is still a problem if the class is universe polymorphic *) Section Embed_ILogic_Pre. Polymorphic Universes A T. Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. diff --git a/test-suite/bugs/closed/bug_4720.v b/test-suite/bugs/closed/bug_4720.v index 704331e784..a870792c39 100644 --- a/test-suite/bugs/closed/bug_4720.v +++ b/test-suite/bugs/closed/bug_4720.v @@ -34,7 +34,7 @@ End WithModPriv. identical by the extraction. In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv - were all causing Anomaly or Assert Failure. This shoud be fixed now. + were all causing Anomaly or Assert Failure. This should be fixed now. *) Require Extraction. diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v deleted file mode 100644 index f238086633..0000000000 --- a/test-suite/bugs/closed/bug_4798.v +++ /dev/null @@ -1,5 +0,0 @@ -(* DO NOT MODIFY THIS FILE DIRECTLY *) -(* It is autogenerated by dev/tools/update-compat.py. *) -Check match 2 with 0 => 0 | S n => n end. -Notation "|" := 1 (compat "8.8"). -Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/bug_4869.v b/test-suite/bugs/closed/bug_4869.v index ac5d7ea287..1fe91de72d 100644 --- a/test-suite/bugs/closed/bug_4869.v +++ b/test-suite/bugs/closed/bug_4869.v @@ -6,7 +6,9 @@ Fail Constraint i = Set. Constraint Set <= i. Constraint Set < i. Fail Constraint i < j. (* undeclared j *) +(* Now a parsing error Fail Constraint i < Type. (* anonymous *) +*) Set Universe Polymorphism. diff --git a/test-suite/bugs/closed/bug_5123.v b/test-suite/bugs/closed/bug_5123.v index 17231bffcf..a4029aeee0 100644 --- a/test-suite/bugs/closed/bug_5123.v +++ b/test-suite/bugs/closed/bug_5123.v @@ -28,6 +28,6 @@ Goal True. opose (@vect_sigT_eqdec _ _ _ _) as H. Unshelve. all:cycle 3. - eapply existT. (*This does no typeclass resultion, which is correct.*) + eapply existT. (*This does no typeclass resolution, which is correct.*) Focus 5. Abort. diff --git a/test-suite/bugs/closed/bug_5149.v b/test-suite/bugs/closed/bug_5149.v index ae32217057..b56abfe42e 100644 --- a/test-suite/bugs/closed/bug_5149.v +++ b/test-suite/bugs/closed/bug_5149.v @@ -36,7 +36,7 @@ Proof. solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail "too early". Undo. - (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) + (** Implicitly at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ]. solve [eapply interpf_SmartVarVar; subst; eassumption]. Undo. diff --git a/test-suite/bugs/closed/bug_808_2411.v b/test-suite/bugs/closed/bug_808_2411.v index 1169b2036b..9fe4c9d503 100644 --- a/test-suite/bugs/closed/bug_808_2411.v +++ b/test-suite/bugs/closed/bug_808_2411.v @@ -2,7 +2,7 @@ Section test. Variable n:nat. Lemma foo: 0 <= n. Proof. -(* declaring an Axiom during a proof makes it immediatly +(* declaring an Axiom during a proof makes it immediately usable, juste as a full Definition. *) Axiom bar : n = 1. rewrite bar. diff --git a/test-suite/bugs/closed/bug_8725.v b/test-suite/bugs/closed/bug_8725.v new file mode 100644 index 0000000000..c888b9e96d --- /dev/null +++ b/test-suite/bugs/closed/bug_8725.v @@ -0,0 +1,2 @@ +Set Warnings "+local-declaration". +Fail Let foo : True. diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v index 21cd770cbb..cd594c660f 100644 --- a/test-suite/bugs/closed/bug_9166.v +++ b/test-suite/bugs/closed/bug_9166.v @@ -1,8 +1,7 @@ -(* DO NOT MODIFY THIS FILE DIRECTLY *) -(* It is autogenerated by dev/tools/update-compat.py. *) Set Warnings "+deprecated". -Notation bar := option (compat "8.8"). +#[deprecated(since = "X", note = "Y")] +Notation bar := option. Definition foo (x: nat) : nat := match x with diff --git a/test-suite/dune b/test-suite/dune index cd33319fa4..041c181d66 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -22,6 +22,7 @@ ../doc/stdlib/index-list.html.template ; For the changelog test ../config/coq_config.py + (source_tree doc/changelog) (package coq) ; For fake_ide (package coqide-server) 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/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v index 0d75d52a31..d2e6794c0b 100644 --- a/test-suite/interactive/ParalITP_smallproofs.v +++ b/test-suite/interactive/ParalITP_smallproofs.v @@ -14,7 +14,7 @@ (* 02110-1301 USA *) -(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful. +(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful. *) Require Export ZArith. @@ -84,7 +84,7 @@ End projection. (*###########################################################################*) -(* Declaring some realtions on natural numbers for stepl and stepr tactics. *) +(* Declaring some relations on natural numbers for stepl and stepr tactics. *) (*###########################################################################*) Lemma le_stepl: forall x y z, le x y -> x=z -> le z y. @@ -173,7 +173,7 @@ Qed. (*###########################################################################*) -(* Declaring some realtions on integers for stepl and stepr tactics. *) +(* Declaring some relations on integers for stepl and stepr tactics. *) (*###########################################################################*) Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z. diff --git a/test-suite/ltac2/notations.v b/test-suite/ltac2/notations.v new file mode 100644 index 0000000000..3d2a875e38 --- /dev/null +++ b/test-suite/ltac2/notations.v @@ -0,0 +1,24 @@ +From Ltac2 Require Import Ltac2. +From Coq Require Import ZArith String List. + +Open Scope Z_scope. + +Check 1 + 1 : Z. + +Ltac2 Notation "ex" arg(constr(nat,Z)) := arg. + +Check (1 + 1)%nat%Z = 1%nat. + +Lemma two : nat. + refine (ex (1 + 1)). +Qed. + +Import ListNotations. +Close Scope list_scope. + +Ltac2 Notation "sl" arg(constr(string,list)) := arg. + +Lemma maybe : list bool. +Proof. + refine (sl ["left" =? "right"]). +Qed. diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh index ed473e5874..76eb0de5aa 100755 --- a/test-suite/misc/changelog.sh +++ b/test-suite/misc/changelog.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash if grep -q -F "is_a_released_version = False" ../config/coq_config.py; then echo "This is not a released version: nothing to test." @@ -7,7 +7,8 @@ fi for d in ../doc/changelog/*; do if [ -d "$d" ]; then - if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then + files=("$d"/*.rst) + if [ "${#files[@]}" != 1 ]; then echo "Fatal: unreleased changelog entries remain in ${d#../}/" echo "Include them in doc/sphinx/changes.rst and remove them from doc/changelog/" exit 1 diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index adabb7a0a0..8447cf10db 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -11,7 +11,7 @@ let evil t f = let te = Declare.definition_entry ~univs:(Monomorphic_entry (ContextSet.singleton u)) tu in - let tc = Declare.declare_constant t (DefinitionEntry te, k) in + let tc = Declare.declare_constant t (Declare.DefinitionEntry te, k) in let tc = mkConst tc in let fe = Declare.definition_entry @@ -19,4 +19,4 @@ let evil t f = ~types:(Term.mkArrowR tc tu) (mkLambda (Context.nameR (Id.of_string "x"), tc, mkRel 1)) in - ignore (Declare.declare_constant f (DefinitionEntry fe, k)) + ignore (Declare.declare_constant f (Declare.DefinitionEntry fe, k)) diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index ef3f056d89..f659fce680 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -1,2 +1,8 @@ #!/bin/sh -if printf "Drop. #use\"include\";; #quit;;\n" | $coqtopbyte 2>&1 | grep -E "Error|Unbound" ; then exit 1; else exit 0; fi + +command -v "${BIN}coqtop.byte" || { echo "Missing coqtop.byte"; exit 1; } + +f=$(mktemp) +printf 'Drop. #use"include";; #quit;;\n' | "${BIN}coqtop.byte" -q 2>&1 | tee "$f" + +if grep -q -E "Error|Unbound" "$f"; then exit 1; fi diff --git a/test-suite/misc/quotation_token.sh b/test-suite/misc/quotation_token.sh new file mode 100755 index 0000000000..6357e8d7ce --- /dev/null +++ b/test-suite/misc/quotation_token.sh @@ -0,0 +1,31 @@ +#!/usr/bin/env bash + +set -e + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +cd misc/quotation_token/ + +coq_makefile -f _CoqProject -o Makefile + +make clean + +make src/quotation_plugin.cma + +TMP=`mktemp` + +if make > $TMP 2>&1; then + echo "should fail" + rm $TMP + exit 1 +fi + +if grep "File.*quotation.v., line 12, characters 6-30" $TMP; then + rm $TMP + exit 0 +else + echo "wong loc: `grep File.*quotation.v $TMP`" + rm $TMP + exit 1 +fi diff --git a/test-suite/misc/quotation_token/.gitignore b/test-suite/misc/quotation_token/.gitignore new file mode 100644 index 0000000000..18da256f3e --- /dev/null +++ b/test-suite/misc/quotation_token/.gitignore @@ -0,0 +1,2 @@ +/Makefile* +/src/quotation.ml diff --git a/test-suite/misc/quotation_token/_CoqProject b/test-suite/misc/quotation_token/_CoqProject new file mode 100644 index 0000000000..1b3e7c6399 --- /dev/null +++ b/test-suite/misc/quotation_token/_CoqProject @@ -0,0 +1,6 @@ +-Q theories Quotation +-I src + +src/quotation.mlg +src/quotation_plugin.mlpack +theories/quotation.v diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg new file mode 100644 index 0000000000..961b170a0d --- /dev/null +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -0,0 +1,12 @@ +{ +open Pcoq.Constr +} +GRAMMAR EXTEND Gram + GLOBAL: operconstr; + + operconstr: LEVEL "0" + [ [ s = QUOTATION "foobar:" -> + { + CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] + ; +END diff --git a/test-suite/misc/quotation_token/src/quotation_plugin.mlpack b/test-suite/misc/quotation_token/src/quotation_plugin.mlpack new file mode 100644 index 0000000000..b372b94b30 --- /dev/null +++ b/test-suite/misc/quotation_token/src/quotation_plugin.mlpack @@ -0,0 +1 @@ +Quotation diff --git a/test-suite/misc/quotation_token/theories/quotation.v b/test-suite/misc/quotation_token/theories/quotation.v new file mode 100644 index 0000000000..66326e89c1 --- /dev/null +++ b/test-suite/misc/quotation_token/theories/quotation.v @@ -0,0 +1,13 @@ + +Declare ML Module "quotation_plugin". + +Definition x := foobar:{{ hello + there +}}. + +Definition y := foobar:{{ another + multi line + thing +}}. +Check foobar:{{ oops + ips }} y. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index dcc8bd7165..29614c032a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -209,7 +209,7 @@ Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun Check exists_mixed x y '(u,t), x+y=0/\u+t=0. Check exists_mixed x y '(z,t), x+y=0/\z+t=0. -(* Check that intermediary let-in are inserted inbetween instances of +(* Check that intermediary let-in are inserted in between instances of the repeated pattern *) Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. diff --git a/test-suite/output/injection.out b/test-suite/output/injection.out new file mode 100644 index 0000000000..ff40a478f3 --- /dev/null +++ b/test-suite/output/injection.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +Unexpected pattern. +The command has indeed failed with message: +Unexpected injection pattern. diff --git a/test-suite/output/injection.v b/test-suite/output/injection.v new file mode 100644 index 0000000000..bfd5a67bf5 --- /dev/null +++ b/test-suite/output/injection.v @@ -0,0 +1,8 @@ +(* Test error messages *) + +Goal forall x, (x,0) = (0, S x) -> x = 0. +Fail intros x H; injection H as [= H'] H''. +Fail intros x H; injection H as H' [= H'']. +intros x H; injection H as [= H' H'']. +exact H'. +Qed. 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/case_polyuniv.v b/test-suite/ssr/case_polyuniv.v new file mode 100644 index 0000000000..8774e191c1 --- /dev/null +++ b/test-suite/ssr/case_polyuniv.v @@ -0,0 +1,12 @@ +Require Import ssreflect. + +Set Universe Polymorphism. + +Cumulative Variant paths {A} (x:A) : A -> Type + := idpath : paths x x. + +Register paths as core.eq.type. +Register idpath as core.eq.refl. + +Lemma case_test (b:bool) : paths b b. +Proof. case B:b; reflexivity. Qed. 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/unfold_fold_polyuniv.v b/test-suite/ssr/unfold_fold_polyuniv.v new file mode 100644 index 0000000000..1a9309bc79 --- /dev/null +++ b/test-suite/ssr/unfold_fold_polyuniv.v @@ -0,0 +1,40 @@ +Require Import ssreflect ssrbool. + +Set Universe Polymorphism. + +Cumulative Variant paths {A} (x:A) : A -> Type + := idpath : paths x x. + +Register paths as core.eq.type. +Register idpath as core.eq.refl. + +Structure type := Pack {sort; op : rel sort}. + +Example unfold_fold (T : type) (x : sort T) (a : op T x x) : op T x x. +Proof. + rewrite /op. rewrite -/(op _ _ _). assumption. +Qed. + +Example pattern_unfold_fold (b:bool) (a := b) : paths a b. +Proof. + rewrite [in X in paths X _]/a. + rewrite -[in X in paths X _]/a. + constructor. +Qed. + +Example unfold_in_hyp (b:bool) (a := b) : unit. +Proof. + assert (paths a a) as A by reflexivity. + rewrite [in X in paths X _]/a in A. + rewrite /a in (B := idpath a). + rewrite [in X in paths _ X]/a in (C := idpath a). + constructor. +Qed. + +Example fold_in_hyp (b:bool) (p := idpath b) : unit. +Proof. + assert (paths (idpath b) (idpath b)) as A by reflexivity. + rewrite -[in X in paths X _]/p in A. + rewrite -[in X in paths _ X]/p in (C := idpath (idpath b)). + constructor. +Qed. 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/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v index 3c427237b4..69ed621877 100644 --- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v @@ -14,7 +14,7 @@ (* 02110-1301 USA *) -(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful. +(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful. *) Require Export ZArith. @@ -84,7 +84,7 @@ End projection. (*###########################################################################*) -(* Declaring some realtions on natural numbers for stepl and stepr tactics. *) +(* Declaring some relations on natural numbers for stepl and stepr tactics. *) (*###########################################################################*) Lemma le_stepl: forall x y z, le x y -> x=z -> le z y. @@ -173,7 +173,7 @@ Qed. (*###########################################################################*) -(* Declaring some realtions on integers for stepl and stepr tactics. *) +(* Declaring some relations on integers for stepl and stepr tactics. *) (*###########################################################################*) Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z. diff --git a/test-suite/success/BidirectionalityHints.v b/test-suite/success/BidirectionalityHints.v new file mode 100644 index 0000000000..284cdc871b --- /dev/null +++ b/test-suite/success/BidirectionalityHints.v @@ -0,0 +1,114 @@ +From Coq Require Import Utf8. +Set Default Proof Using "Type". + +Module SimpleExamples. + +Axiom c : bool -> nat. +Coercion c : bool >-> nat. +Inductive Boxed A := Box (a : A). +Arguments Box {A} & a. +Check Box true : Boxed nat. + +(* Here we check that there is no regression due e.g. to refining arguments + in the wrong order *) +Axiom f : forall b : bool, (if b then bool else nat) -> Type. +Check f true true : Type. +Arguments f & _ _. +Check f true true : Type. + +End SimpleExamples. + +Module Issue7910. + +Local Set Universe Polymorphism. + +(** Telescopes *) +Inductive tele : Type := + | TeleO : tele + | TeleS {X} (binder : X → tele) : tele. + +Arguments TeleS {_} _. + +(** The telescope version of Coq's function type *) +Fixpoint tele_fun (TT : tele) (T : Type) : Type := + match TT with + | TeleO => T + | TeleS b => ∀ x, tele_fun (b x) T + end. + +Notation "TT -t> A" := + (tele_fun TT A) (at level 99, A at level 200, right associativity). + +(** An eliminator for elements of [tele_fun]. + We use a [fix] because, for some reason, that makes stuff print nicer + in the proofs in iris:bi/lib/telescopes.v *) +Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y) + : (TT -t> X) → Y := + (fix rec {TT} : (TT -t> X) → Y := + match TT as TT return (TT -t> X) → Y with + | TeleO => λ x : X, base x + | TeleS b => λ f, step (λ x, rec (f x)) + end) TT. +Arguments tele_fold {_ _ !_} _ _ _ /. + +(** A sigma-like type for an "element" of a telescope, i.e. the data it + takes to get a [T] from a [TT -t> T]. *) +Inductive tele_arg : tele → Type := +| TargO : tele_arg TeleO +(* the [x] is the only relevant data here *) +| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder). + +Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T := + λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T := + match a in tele_arg TT return (TT -t> T) → T with + | TargO => λ t : T, t + | TargS x a => λ f, rec a (f x) + end) TT a f. +Arguments tele_app {!_ _} & _ !_ /. + +Coercion tele_arg : tele >-> Sortclass. +Coercion tele_app : tele_fun >-> Funclass. + +(** Operate below [tele_fun]s with argument telescope [TT]. *) +Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U := + match TT as TT return (TT → U) → TT -t> U with + | TeleO => λ F, F TargO + | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *) + tele_bind (λ a, F (TargS x a)) + end. +Arguments tele_bind {_ !_} _ /. + +(** Telescopic quantifiers *) +Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop := + tele_fold (λ (T : Type) (b : T → Prop), ∀ x : T, b x) (λ x, x) (tele_bind Ψ). +Arguments tforall {!_} _ /. +Definition texist {TT : tele} (Ψ : TT → Prop) : Prop := + tele_fold ex (λ x, x) (tele_bind Ψ). +Arguments texist {!_} _ /. + +Notation "'∀..' x .. y , P" := (tforall (λ x, .. (tforall (λ y, P)) .. )) + (at level 200, x binder, y binder, right associativity, + format "∀.. x .. y , P"). +Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. )) + (at level 200, x binder, y binder, right associativity, + format "∃.. x .. y , P"). + +(** The actual test case *) +Definition test {TT : tele} (t : TT → Prop) : Prop := + ∀.. x, t x ∧ t x. + +Notation "'[TEST' x .. z , P ']'" := + (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (tele_app (λ x, .. (λ z, P) ..))) + (x binder, z binder). +Notation "'[TEST2' x .. z , P ']'" := + (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (tele_app (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (λ x, .. (λ z, P) ..))) + (x binder, z binder). + +Check [TEST (x y : nat), x = y]. + +Check [TEST2 (x y : nat), x = y]. + +End Issue7910. diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v index 69fca48e24..ba6bf3bba2 100644 --- a/test-suite/success/Case15.v +++ b/test-suite/success/Case15.v @@ -20,7 +20,7 @@ Definition test (B : Boite) := | boite false (n, m) => n + m end. -(* Check lazyness of compilation ... future work +(* Check laziness of compilation ... future work Inductive I : Set := c : (b:bool)(if b then bool else nat)->I. Check [x] diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v index be9ca8d41b..6bea435090 100644 --- a/test-suite/success/Case18.v +++ b/test-suite/success/Case18.v @@ -1,7 +1,10 @@ (* Check or-patterns *) +(* Non-interference with Numbers divisibility. *) +Reserved Notation "( p | q )" (at level 0). + Definition g x := - match x with ((((1 as x),_) | (_,x)), (_,(2 as y))|(y,_)) => (x,y) end. + match x with ((((1 as x),_) | (_,x)), ((_,(2 as y)) | (y,_))) => (x,y) end. Check (refl_equal _ : g ((1,2),(3,4)) = (1,3)). diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 8d9edbd62d..02e15b8ee2 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -62,7 +62,7 @@ Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option n (* -------------------------------------------------------------------- *) (* Example to test patterns matching on dependent families *) -(* This exemple extracted from the developement done by Nacira Chabane *) +(* This exemple extracted from the development done by Nacira Chabane *) (* (equipe Paris 6) *) (* -------------------------------------------------------------------- *) @@ -298,7 +298,7 @@ End Version1. (* ------------------------------------------------------------------*) -(* Initial exemple (without patterns) *) +(* Initial example (without patterns) *) (*-------------------------------------------------------------------*) Module Version2. 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/Discriminate_HoTT.v b/test-suite/success/Discriminate_HoTT.v new file mode 100644 index 0000000000..2a5e083d56 --- /dev/null +++ b/test-suite/success/Discriminate_HoTT.v @@ -0,0 +1,89 @@ +(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter") -*- *) + +(* This file tests the discriminate tactic compatibility with HoTT. + The first part of the file will setup a mini HoTT environment. + Afterwards a number of tests are performed. The tests are basically + copied from the Discriminate.v test file. *) + +Unset Elimination Schemes. + +Set Universe Polymorphism. + +Declare ML Module "ltac_plugin". + +Global Set Default Proof Mode "Classic". + +Notation "x -> y" := (forall (_:x), y) (at level 99, right associativity, y at level 200). + +Cumulative Variant paths {A} (a:A) : A -> Type + := idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Scheme paths_ind := Induction for paths Sort Type. +Arguments paths_ind [A] a P f y p. + +Notation "x = y :> A" := (@paths A x y) (at level 70, y at next level, no associativity). +Notation "x = y" := (x = y :>_) (at level 70, no associativity). + +Register paths as core.identity.type. +Register idpath as core.identity.refl. +Register paths_ind as core.identity.ind. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. +Arguments inverse {A x y} p : simpl nomatch. +Register inverse as core.identity.sym. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. +Arguments concat {A x y z} p q : simpl nomatch. +Register concat as core.identity.trans. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +Arguments ap {A B} f {x y} p. +Register ap as core.identity.congr. + +Variant Empty : Type :=. + +Register Empty as core.False.type. + +Variant Unit : Type := tt. + +Register Unit as core.True.type. +Register tt as core.True.I. + +Variant Bool : Type := true | false. + +Inductive nat : Type := O | S (n:nat). + +(*********** Test discriminate tactic below. ***************) + +Goal O = S O -> Empty. + discriminate 1. +Qed. + +Goal forall H : O = S O, H = H. + discriminate H. +Qed. + +Goal O = S O -> Unit. +intros. discriminate H. Qed. +Goal O = S O -> Unit. +intros. Ltac g x := discriminate x. g H. Qed. + +Goal (forall x y : nat, x = y -> x = S y) -> Unit. +intros. +try discriminate (H O) || exact tt. +Qed. + +Goal (forall x y : nat, x = y -> x = S y) -> Unit. +intros. ediscriminate (H O). instantiate (1:=O). Abort. + +(* Check discriminate on types with local definitions *) + +Inductive A := B (T := Unit) (x y : Bool) (z := x). +Goal forall x y, B x true = B y false -> Empty. +discriminate. +Qed. 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/Hints.v b/test-suite/success/Hints.v index 2f13b7c225..e96a5f9048 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -175,7 +175,7 @@ End HintCut. (* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *) -(* e.g. those tactics when considering a goal with existential varibles *) +(* e.g. those tactics when considering a goal with existential variables *) (* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *) (* See this Coq club post for more detail: *) (* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index ee540d7109..1dbeaf3e1f 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -179,7 +179,7 @@ exact Logic.I. Qed. (* Up to September 2014, H0 below was renamed called H1 because of a collision - with the automaticallly generated names for equations. + with the automatically generated names for equations. (example taken from CoLoR) *) Inductive term := Var | Fun : term -> term -> term. diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v new file mode 100644 index 0000000000..22fb09526d --- /dev/null +++ b/test-suite/success/LocalDefinition.v @@ -0,0 +1,53 @@ +(* Test consistent behavior of Local Definition (#8722) *) + +(* Test consistent behavior of Local Definition wrt Admitted *) + +Module TestAdmittedVisibility. + Module A. + Let a1 : nat. Admitted. (* Suppose to behave like a "Local Definition" *) + Local Definition b1 : nat. Admitted. (* Told to be a "Local Definition" *) + Local Definition c1 := 0. + Local Parameter d1 : nat. + Section S. + Let a2 : nat. Admitted. (* Told to be turned into a toplevel assumption *) + Local Definition b2 : nat. Admitted. (* Told to be a "Local Definition" *) + Local Definition c2 := 0. + Local Parameter d2 : nat. + End S. + End A. + Import A. + Fail Check a1. (* used to be accepted *) + Fail Check b1. (* used to be accepted *) + Fail Check c1. + Fail Check d1. + Fail Check a2. (* used to be accepted *) + Fail Check b2. (* used to be accepted *) + Fail Check c2. + Fail Check d2. +End TestAdmittedVisibility. + +(* Test consistent behavior of Local Definition wrt automatic declaration of instances *) + +Module TestVariableAsInstances. + Module Test1. + Set Typeclasses Axioms Are Instances. + Class U. + Local Parameter b : U. + Definition testU := _ : U. (* _ resolved *) + + Class T. + Variable a : T. (* warned to be the same as "Local Parameter" *) + Definition testT := _ : T. (* _ resolved *) + End Test1. + + Module Test2. + Unset Typeclasses Axioms Are Instances. + Class U. + Local Parameter b : U. + Fail Definition testU := _ : U. (* _ unresolved *) + + Class T. + Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *) + Fail Definition testT := _ : T. (* used to succeed *) + End Test2. +End TestVariableAsInstances. diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v new file mode 100644 index 0000000000..d313ba0aa4 --- /dev/null +++ b/test-suite/success/NotationDeprecation.v @@ -0,0 +1,62 @@ +Module Syndefs. + +#[deprecated(since = "8.8", note = "Do not use.")] +Notation foo := Prop. + +Notation bar := Prop (compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Notation zar := Prop (compat "8.8"). + +Check foo. +Check bar. + +Set Warnings "+deprecated". + +Fail Check foo. +Fail Check bar. + +End Syndefs. + +Module Notations. + +#[deprecated(since = "8.8", note = "Do not use.")] +Notation "!!" := Prop. + +Notation "##" := Prop (compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Notation "**" := Prop (compat "8.8"). + +Check !!. +Check ##. + +Set Warnings "+deprecated". + +Fail Check !!. +Fail Check ##. + +End Notations. + +Module Infix. + +#[deprecated(since = "8.8", note = "Do not use.")] +Infix "!!" := plus (at level 1). + +Infix "##" := plus (at level 1, compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Infix "**" := plus (at level 1, compat "8.8"). + +Check (_ !! _). +Check (_ ## _). + +Set Warnings "+deprecated". + +Fail Check (_ !! _). +Fail Check (_ ## _). + +End Infix. diff --git a/test-suite/success/Reordering.v b/test-suite/success/Reordering.v index de9b997590..98759264e5 100644 --- a/test-suite/success/Reordering.v +++ b/test-suite/success/Reordering.v @@ -1,7 +1,7 @@ (* Testing the reordering of hypothesis required by pattern, fold and change. *) Goal forall (A:Set) (x:A) (A':=A), True. intros. -fold A' in x. (* suceeds: x is moved after A' *) +fold A' in x. (* succeeds: x is moved after A' *) Undo. pattern A' in x. Undo. 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/extraction_dep.v b/test-suite/success/extraction_dep.v index fb0adabae9..c566a6db9f 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -34,7 +34,7 @@ Definition testAbis := Abis.u + Abis.y. Recursive Extraction testAbis. (* without: A B v w x *) Extraction TestCompile testAbis. -(** 2) With signature, we only keep elements mentionned in signature. *) +(** 2) With signature, we only keep elements mentioned in signature. *) Module Type SIG. Parameter u : nat. diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 0951c5c8d4..ae834e7696 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -13,13 +13,15 @@ Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true. Proof. do 2 dup. - repeat split. - 2, 4-99, 100-3:idtac. + Fail 7:idtac. + Fail 2-1:idtac. + 1,2,4-6:idtac. 2-5:exact One. par:exact Zero. - repeat split. 3-6:swap 1 4. 1-5:swap 1 5. - 0-4:exact One. + 1-4:exact One. all:exact Zero. - repeat split. 1, 3:exact Zero. @@ -34,7 +36,7 @@ Qed. Goal True -> True. Proof. - intros y; only 1-2 : repeat idtac. + intros y. 1-1:match goal with y : _ |- _ => let x := y in idtac x end. Fail 1-1:let x := y in idtac x. 1:let x := y in idtac x. diff --git a/test-suite/success/if.v b/test-suite/success/if.v index c81d2b9bf1..68d26ac8df 100644 --- a/test-suite/success/if.v +++ b/test-suite/success/if.v @@ -1,4 +1,4 @@ -(* The synthesis of the elimination predicate may fail if algebric *) +(* The synthesis of the elimination predicate may fail if algebraic *) (* universes are not cautiously treated *) Check (fun b : bool => if b then Type else nat). 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 *) diff --git a/test-suite/unit-tests/ide/lex_tests.ml b/test-suite/unit-tests/ide/lex_tests.ml new file mode 100644 index 0000000000..3082acdf1f --- /dev/null +++ b/test-suite/unit-tests/ide/lex_tests.ml @@ -0,0 +1,50 @@ +open Utest + +let log_out_ch = open_log_out_ch __FILE__ + +let lex s = + let n = + let last = String.length s - 1 in + if s.[last] = '.' then Some last else None in + let stop = ref None in + let f i _ = assert(!stop = None); stop := Some i in + begin try Coq_lex.delimit_sentences f s + with Coq_lex.Unterminated -> () end; + if n <> !stop then begin + let p_opt = function None -> "None" | Some i -> "Some " ^ string_of_int i in + Printf.fprintf log_out_ch "ERROR: %S\nEXPECTED: %s\nGOT: %s\n" s (p_opt n) (p_opt !stop) + end; + n = !stop + +let i2s i = "test at line: " ^ string_of_int i + +let tests = [ + + mk_bool_test (i2s __LINE__) "no quotation" @@ lex + "foo.+1 bar." + ; + mk_bool_test (i2s __LINE__) "quotation" @@ lex + "foo constr:(xxx)." + ; + mk_bool_test (i2s __LINE__) "quotation with dot" @@ lex + "foo constr:(xxx. yyy)." + ; + mk_bool_test (i2s __LINE__) "quotation with dot double paren" @@ lex + "foo constr:((xxx. (foo.+1 ) \")\" yyy))." + ; + mk_bool_test (i2s __LINE__) "quotation with dot paren [" @@ lex + "foo constr:[xxx. (foo.+1 ) \")\" yyy]." + ; + mk_bool_test (i2s __LINE__) "quotation with dot double paren [" @@ lex + "foo constr:[[xxx. (foo.+1 ) \")\" yyy]]." + ; + mk_bool_test (i2s __LINE__) "quotation with dot triple paren [" @@ lex + "foo constr:[[[xxx. (foo.+1 @@ [] ) \"]])\" yyy]]]." + ; + mk_bool_test (i2s __LINE__) "quotation nesting {" @@ lex + "bar:{{ foo {{ hello. }} }}." + ; + +] + +let _ = run_tests __FILE__ log_out_ch tests diff --git a/test-suite/vio/section.v b/test-suite/vio/section.v new file mode 100644 index 0000000000..0e7722516a --- /dev/null +++ b/test-suite/vio/section.v @@ -0,0 +1,12 @@ +Section Foo. + Variable A : Type. + + Definition bla := A. + + Variable B : bla. + + Lemma blu : {X:Type & X}. + Proof using A B. + exists bla;exact B. + Qed. +End Foo. |