diff options
Diffstat (limited to 'test-suite')
90 files changed, 459 insertions, 99 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 552d007f85..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}!"; \ 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_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_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_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 041c181d66..6ab2988331 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -20,6 +20,14 @@ ../dev/header.ml ../dev/tools/update-compat.py ../doc/stdlib/index-list.html.template + ; For the misc/printers.sh test + ../dev/incdir_dune + ../dev/base_include + ../dev/inc_ltac_dune + ../dev/include_printers + ../dev/include_dune + ../dev/top_printers.ml + ../dev/vm_printers.ml ; For the changelog test ../config/coq_config.py (source_tree doc/changelog) 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/ltac2/compat.v b/test-suite/ltac2/compat.v index 489fa638e4..9c11d19c27 100644 --- a/test-suite/ltac2/compat.v +++ b/test-suite/ltac2/compat.v @@ -27,6 +27,19 @@ Fail Ltac2 bar nay := ltac1:(discriminate nay). Fail Ltac2 pose1 (v : constr) := ltac1:(pose $v). +(** Variables explicitly crossing the boundary must satisfy typing properties *) +Goal True. +Proof. +(* Wrong type *) +Fail ltac1:(x |- idtac) 0. +(* OK, and runtime has access to variable *) +ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)). + +(* Same for ltac1val *) +Fail Ltac1.run (ltac1val:(x |- idtac) 0). +Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))). +Abort. + (** Test calls to Ltac2 from Ltac1 *) Set Default Proof Mode "Classic". 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..8c4808a755 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -1,17 +1,16 @@ open Names -let evil t f = +let evil name name_f = let open Univ in let open Entries in - let open Decl_kinds in let open Constr in - let k = IsDefinition Definition in + let kind = Decls.(IsDefinition Definition) in let u = Level.var 0 in let tu = mkType (Universe.make u) in 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 ~name ~kind (Declare.DefinitionEntry te) in let tc = mkConst tc in let fe = Declare.definition_entry @@ -19,4 +18,5 @@ 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)) + let _ : Constant.t = Declare.declare_constant ~name:name_f ~kind (Declare.DefinitionEntry fe) in + () diff --git a/test-suite/misc/printers.sh b/test-suite/misc/printers.sh index f659fce680..f2bf6b8681 100755 --- a/test-suite/misc/printers.sh +++ b/test-suite/misc/printers.sh @@ -3,6 +3,18 @@ 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 [ -n "$INSIDE_DUNE" ]; then + printf 'Drop.\n#directory "../dev";;\n#use "include_dune";;\n#quit;;\n' | coqtop.byte -q + else + # -I ../dev is not needed when compiled with -local (usual dev + # setup), but is needed for CI testing. + printf 'Drop. #use "include";; #quit;;\n' | "${BIN}coqtop.byte" -I ../dev -q + fi +} 2>&1 | tee "$f" -if grep -q -E "Error|Unbound" "$f"; then exit 1; fi +# if there's an issue in base_include 'go' won't be defined +# if there's an issue in include_printers it will be an undefined printer +if ! grep -q -F 'val go : unit -> unit = <fun>' "$f" || + 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-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out new file mode 100644 index 0000000000..2eadd22db8 --- /dev/null +++ b/test-suite/output-coqtop/ShowGoal.out @@ -0,0 +1,73 @@ +
+Coq < 1 subgoal
+
+ ============================
+ forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k
+
+x <
+x < 1 focused subgoal
+(shelved: 1)
+
+ i : nat
+ ============================
+ exists k : nat, i = ?j /\ ?j = k /\ i = k
+
+x < 1 focused subgoal
+(shelved: 2)
+
+ i : nat
+ ============================
+ i = ?j /\ ?j = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 2)
+
+ i : nat
+ ============================
+ i = ?j
+
+subgoal 2 is:
+ ?j = ?k /\ i = ?k
+
+x < 1 focused subgoal
+(shelved: 1)
+
+ i : nat
+ ============================
+ i = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 1)
+
+ i : nat
+ ============================
+ i = ?k
+
+subgoal 2 is:
+ i = ?k
+
+x < 1 subgoal
+
+ i : nat
+ ============================
+ i = i
+
+x < goal ID 16 at state 5
+
+ i : nat
+ ============================
+ i = ?j /\ ?j = ?k /\ i = ?k
+
+x < goal ID 16 at state 7
+
+ i : nat
+ ============================
+ i = i /\ i = ?k /\ i = ?k
+
+x < goal ID 16 at state 9
+
+ i : nat
+ ============================
+ i = i /\ i = i /\ i = i
+
+x <
diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v new file mode 100644 index 0000000000..9545254770 --- /dev/null +++ b/test-suite/output-coqtop/ShowGoal.v @@ -0,0 +1,11 @@ +Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k. +Proof using. + eexists. + eexists. + split. + trivial. + split. + trivial. +Show Goal 16 at 5. +Show Goal 16 at 7. +Show Goal 16 at 9. diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out index 2a7ce806d7..dc793598a9 100644 --- a/test-suite/output/relaxed_ambiguous_paths.out +++ b/test-suite/output/relaxed_ambiguous_paths.out @@ -1,5 +1,7 @@ File "stdin", line 10, characters 0-28: -Warning: Ambiguous paths: [ac; cd] : A >-> D [ambiguous-paths,typechecker] +Warning: +New coercion path [ac; cd] : A >-> D is ambiguous with existing +[ab; bd] : A >-> D. [ambiguous-paths,typechecker] [ab] : A >-> B [ab; bd] : A >-> D [ac] : A >-> C @@ -20,8 +22,9 @@ Warning: Ambiguous paths: [ac; cd] : A >-> D [ambiguous-paths,typechecker] [D_B] : D >-> B [D_C] : D >-> C File "stdin", line 103, characters 0-86: -Warning: Ambiguous paths: [D_C; C_A'] : D >-> A' -[ambiguous-paths,typechecker] +Warning: +New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing +[D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker] [A'_A] : A' >-> A [B_A'] : B >-> A' [B_A'; A'_A] : B >-> A 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/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/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 *) 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 |