diff options
Diffstat (limited to 'test-suite')
88 files changed, 1118 insertions, 100 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 5ab4cacdaf..beb80a3dfd 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -27,8 +27,8 @@ # Default value when called from a freshly compiled Coq, but can be # easily overridden -LIB := $(shell cd ..; pwd) -BIN := $(LIB)/bin/ +LIB := .. +BIN := $(shell cd ..; pwd)/bin/ coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite @@ -170,6 +170,7 @@ summary.log: report: summary.log $(HIDE)./save-logs.sh $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi + $(HIDE)if [ -n "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### @@ -293,7 +294,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) | grep -v "^<W>" \ | sed 's/File "[^"]*"/File "stdin"/' \ > $$tmpoutput; \ - diff -u $*.out $$tmpoutput 2>&1; R=$$?; times; \ + diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -328,7 +329,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out -e 's/\s*[-+]inf\s*//g' \ -e 's/^[^a-zA-Z]*//' \ $*.out | sort > $$tmpexpected; \ - diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ + diff --strip-trailing-cr -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -445,7 +446,7 @@ ide : $(patsubst %.fake,%.fake.log,$(wildcard ide/*.fake)) @echo "TEST $<" $(HIDE){ \ echo $(call log_intro,$<); \ - $(BIN)fake_ide $< "$(BIN)coqtop -coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ + $(BIN)fake_ide $< "-coqlib $(LIB) -boot -async-proofs on -async-proofs-tactic-error-resilience off -async-proofs-command-error-resilience off" 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v new file mode 100644 index 0000000000..9265b60c17 --- /dev/null +++ b/test-suite/bugs/closed/4720.v @@ -0,0 +1,46 @@ +(** Bug 4720 : extraction and "with" in module type *) + +Module Type A. + Parameter t : Set. +End A. + +Module A_instance <: A. + Definition t := nat. +End A_instance. + +Module A_private : A. + Definition t := nat. +End A_private. + +Module Type B. +End B. + +Module Type C (b : B). + Declare Module a : A. +End C. + +Module WithMod (a' : A) (b' : B) (c' : C b' with Module a := A_instance). +End WithMod. + +Module WithDef (a' : A) (b' : B) (c' : C b' with Definition a.t := nat). +End WithDef. + +Module WithModPriv (a' : A) (b' : B) (c' : C b' with Module a := A_private). +End WithModPriv. + +(* The initial bug report was concerning the extraction of WithModPriv + in Coq 8.4, which was suboptimal: it was compiling, but could have been + turned into some faulty code since A_private and c'.a were not seen as + 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. +*) + +Require Extraction. + +Recursive Extraction WithMod. + +Recursive Extraction WithDef. + +Recursive Extraction WithModPriv. diff --git a/test-suite/bugs/closed/4844.v b/test-suite/bugs/closed/4844.v new file mode 100644 index 0000000000..f140939ccd --- /dev/null +++ b/test-suite/bugs/closed/4844.v @@ -0,0 +1,47 @@ + +(* Bug report 4844 (and 4824): + The Haskell extraction was erroneously considering [Any] and + [()] as convertible ([Tunknown] an [Tdummy] internally). *) + +(* A value with inner logical parts. + Its extracted type will be [Sum () ()]. *) + +Definition semilogic : True + True := inl I. + +(* Higher-order record, whose projection [ST] isn't expressible + as an Haskell (or OCaml) type. Hence [ST] is extracted as the + unknown type [Any] in Haskell. *) + +Record SomeType := { ST : Type }. + +Definition SomeTrue := {| ST := True |}. + +(* A first version of the issue: + [abstrSum] is extracted as [Sum Any Any], so an unsafeCoerce + is required to cast [semilogic] into [abstrSum SomeTrue]. *) + +Definition abstrSum (t : SomeType) := ((ST t) + (ST t))%type. + +Definition semilogic' : abstrSum SomeTrue := semilogic. + +(* A deeper version of the issue. + In the previous example, the extraction could have reduced + [abstrSum SomeTrue] into [True+True], solving the issue. + It might do so in future versions. But if we put an inductive + in the way, a reduction isn't helpful. *) + +Inductive box (t : SomeType) := Box : ST t + ST t -> box t. + +Definition boxed_semilogic : box SomeTrue := + Box SomeTrue semilogic. + +Require Extraction. +Extraction Language Haskell. +Recursive Extraction semilogic' boxed_semilogic. +(* Warning! To fully check that this bug is still closed, + you should run ghc on the extracted code: + +Extraction "bug4844.hs" semilogic' boxed_semilogic. +ghc bug4844.hs + +*) diff --git a/test-suite/bugs/closed/5177.v b/test-suite/bugs/closed/5177.v new file mode 100644 index 0000000000..231d103a59 --- /dev/null +++ b/test-suite/bugs/closed/5177.v @@ -0,0 +1,21 @@ +(* Bug 5177 https://coq.inria.fr/bug/5177 : + Extraction and module type containing application and "with" *) + +Module Type T. + Parameter t: Type. +End T. + +Module Type A (MT: T). + Parameter t1: Type. + Parameter t2: Type. + Parameter bar: MT.t -> t1 -> t2. +End A. + +Module MakeA(MT: T): A MT with Definition t1 := nat. + Definition t1 := nat. + Definition t2 := nat. + Definition bar (m: MT.t) (x:t1) := x. +End MakeA. + +Require Extraction. +Recursive Extraction MakeA. diff --git a/test-suite/bugs/closed/5205.v b/test-suite/bugs/closed/5205.v new file mode 100644 index 0000000000..406f37a4b1 --- /dev/null +++ b/test-suite/bugs/closed/5205.v @@ -0,0 +1,6 @@ +Definition foo (n : nat) (m : nat) : nat := m. + +Arguments foo {_} _, _ _. + +Check foo 1 1. +Check foo (n:=1) 1. diff --git a/test-suite/bugs/closed/5365.v b/test-suite/bugs/closed/5365.v new file mode 100644 index 0000000000..be360d24d2 --- /dev/null +++ b/test-suite/bugs/closed/5365.v @@ -0,0 +1,13 @@ + +Inductive TupleT : nat -> Type := +| nilT : TupleT 0 +| consT {n} A : (A -> TupleT n) -> TupleT (S n). + +Inductive Tuple : forall n, TupleT n -> Type := + nil : Tuple _ nilT +| cons {n A} (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F). + +Inductive TupleMap : forall n, TupleT n -> TupleT n -> Type := + tmNil : TupleMap _ nilT nilT +| tmCons {n} {A B : Type} (F : A -> TupleT n) (G : B -> TupleT n) + : (forall x, sigT (fun y => TupleMap _ (F x) (G y))) -> TupleMap _ (consT A F) (consT B G). diff --git a/test-suite/bugs/closed/5618.v b/test-suite/bugs/closed/5618.v new file mode 100644 index 0000000000..ab88a88f44 --- /dev/null +++ b/test-suite/bugs/closed/5618.v @@ -0,0 +1,9 @@ +Require Import FunInd. + +Function test {T} (v : T) (x : nat) : nat := + match x with + | 0 => 0 + | S x' => test v x' + end. + +Check R_test_complete.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5641.v b/test-suite/bugs/closed/5641.v new file mode 100644 index 0000000000..9f3246f33d --- /dev/null +++ b/test-suite/bugs/closed/5641.v @@ -0,0 +1,6 @@ +Set Universe Polymorphism. + +Definition foo@{i j} (A : Type@{i}) : Type@{j}. +Proof. +abstract (exact ltac:(abstract (exact A))). +Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_123.v b/test-suite/bugs/closed/HoTT_coq_123.v index cd9cad4064..7bed956f3e 100644 --- a/test-suite/bugs/closed/HoTT_coq_123.v +++ b/test-suite/bugs/closed/HoTT_coq_123.v @@ -104,11 +104,15 @@ Record Functor (C D : PreCategory) := morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. +(** Workaround to simpl losing universe constraints, see bug #5645. *) +Ltac simpl' := + simpl; match goal with [ |- ?P ] => let T := type of P in idtac end. + Global Instance trunc_forall `{Funext} `{P : A -> Type} `{forall a, IsTrunc n (P a)} : IsTrunc n (forall a, P a) | 100. Proof. generalize dependent P. - induction n as [ | n' IH]; (simpl; intros P ?). + induction n as [ | n' IH]; (simpl'; intros P ?). - admit. - pose (fun f g => trunc_equiv (@apD10 A P f g) ^-1); admit. Defined. diff --git a/test-suite/coq-makefile/arg/run.sh b/test-suite/coq-makefile/arg/run.sh index e98da17c78..e7de90ff2f 100755 --- a/test-suite/coq-makefile/arg/run.sh +++ b/test-suite/coq-makefile/arg/run.sh @@ -1,9 +1,7 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make diff --git a/test-suite/coq-makefile/compat-subdirs/run.sh b/test-suite/coq-makefile/compat-subdirs/run.sh index 28d9878f9b..221dcd7bf8 100755 --- a/test-suite/coq-makefile/compat-subdirs/run.sh +++ b/test-suite/coq-makefile/compat-subdirs/run.sh @@ -1,9 +1,8 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh + coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index e8291c89da..1feff7479b 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -1,17 +1,15 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh index e8291c89da..1feff7479b 100755 --- a/test-suite/coq-makefile/coqdoc2/run.sh +++ b/test-suite/coq-makefile/coqdoc2/run.sh @@ -1,17 +1,15 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/extend-subdirs/run.sh b/test-suite/coq-makefile/extend-subdirs/run.sh index ea5792a937..221dcd7bf8 100755 --- a/test-suite/coq-makefile/extend-subdirs/run.sh +++ b/test-suite/coq-makefile/extend-subdirs/run.sh @@ -1,10 +1,8 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec test -f "subdir/done" diff --git a/test-suite/coq-makefile/latex1/run.sh b/test-suite/coq-makefile/latex1/run.sh index 214a9d5b28..b2c5d5669b 100755 --- a/test-suite/coq-makefile/latex1/run.sh +++ b/test-suite/coq-makefile/latex1/run.sh @@ -1,13 +1,11 @@ #!/usr/bin/env bash -#set -x -set -e - if which pdflatex; then . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec make all.pdf diff --git a/test-suite/coq-makefile/merlin1/run.sh b/test-suite/coq-makefile/merlin1/run.sh index 752c0c2cea..1f262a9390 100755 --- a/test-suite/coq-makefile/merlin1/run.sh +++ b/test-suite/coq-makefile/merlin1/run.sh @@ -1,11 +1,9 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make .merlin cat > desired <<EOT B src diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh index 10a200ddee..51669f28f5 100755 --- a/test-suite/coq-makefile/mlpack1/run.sh +++ b/test-suite/coq-makefile/mlpack1/run.sh @@ -1,16 +1,14 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh index 10a200ddee..51669f28f5 100755 --- a/test-suite/coq-makefile/mlpack2/run.sh +++ b/test-suite/coq-makefile/mlpack2/run.sh @@ -1,16 +1,14 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh index 3cd1ac305f..d3bb53106d 100755 --- a/test-suite/coq-makefile/multiroot/run.sh +++ b/test-suite/coq-makefile/multiroot/run.sh @@ -1,19 +1,17 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh cp -r theories theories2 mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" make install-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index 9f6295d644..3bec11cb75 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -1,19 +1,17 @@ #!/usr/bin/env bash -#set -x -set -e - NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true if [[ `which ocamlopt` && $NATIVECOMP ]]; then . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/only/run.sh b/test-suite/coq-makefile/only/run.sh index 2ea3deffb7..8cf04bf2cd 100755 --- a/test-suite/coq-makefile/only/run.sh +++ b/test-suite/coq-makefile/only/run.sh @@ -1,11 +1,9 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make only TGTS="src/test.cmi src/test_aux.cmi" -j2 test -f src/test.cmi test -f src/test_aux.cmi diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh index 6301aa03c0..88606cd473 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -27,6 +27,7 @@ let _ = Pre_env.empty_env EOT ${COQBIN}coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf if make VERBOSE=1; then # make command should have failed (but didn't) diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh index 991fb4a61d..939ef9c7b7 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh @@ -28,5 +28,6 @@ let _ = Pre_env.empty_env EOT ${COQBIN}coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make VERBOSE=1 diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh index c2d47166fe..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin1/run.sh +++ b/test-suite/coq-makefile/plugin1/run.sh @@ -1,17 +1,15 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh index c2d47166fe..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin2/run.sh +++ b/test-suite/coq-makefile/plugin2/run.sh @@ -1,17 +1,15 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh index c2d47166fe..5433d9e92d 100755 --- a/test-suite/coq-makefile/plugin3/run.sh +++ b/test-suite/coq-makefile/plugin3/run.sh @@ -1,17 +1,15 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh mv src/test_plugin.mlpack src/test_plugin.mllib coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" #make debug -(cd `find tmp -name user-contrib`; find .) | sort > actual +(cd `find tmp -name user-contrib` && find .) | sort > actual sort > desired <<EOT . ./test diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index c952d41a30..803fe8029a 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -1,3 +1,5 @@ +set -e +set -o pipefail export PATH=$COQBIN:$PATH diff --git a/test-suite/coq-makefile/timing/after/Fast.v b/test-suite/coq-makefile/timing/after/Fast.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/after/Fast.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/after/Slow.v b/test-suite/coq-makefile/timing/after/Slow.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/Slow.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/after/_CoqProject b/test-suite/coq-makefile/timing/after/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/after/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired new file mode 100644 index 0000000000..729de2f366 --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-after.log.desired @@ -0,0 +1,16 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP Fast.v +COQDEP Slow.v +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.04, user: 0.02, sys: 0.01, mem: 45512 ko) +COQC Fast.v +Fast (real: 0.41, user: 0.37, sys: 0.04, mem: 395200 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired new file mode 100644 index 0000000000..b25bc3683c --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-before.log.desired @@ -0,0 +1,16 @@ +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQDEP Fast.v +COQDEP Slow.v +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' +COQC Slow.v +Slow (real: 0.40, user: 0.35, sys: 0.04, mem: 394968 ko) +COQC Fast.v +Fast (real: 0.04, user: 0.03, sys: 0.00, mem: 46564 ko) +Makefile:69: warning: undefined variable '*' +Makefile:204: warning: undefined variable 'DSTROOT' diff --git a/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired new file mode 100644 index 0000000000..56815d241e --- /dev/null +++ b/test-suite/coq-makefile/timing/after/time-of-build-both.log.desired @@ -0,0 +1,6 @@ +After | File Name | Before || Change | % Change +-------------------------------------------------------- +0m00.38s | Total | 0m00.39s || -0m00.01s | -2.56% +-------------------------------------------------------- +0m00.35s | Slow | 0m00.02s || +0m00.32s | +1649.99% +0m00.03s | Fast | 0m00.37s || -0m00.34s | -91.89%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/aggregate/Fast.v b/test-suite/coq-makefile/timing/aggregate/Fast.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/Fast.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/aggregate/Slow.v b/test-suite/coq-makefile/timing/aggregate/Slow.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/Slow.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/aggregate/_CoqProject b/test-suite/coq-makefile/timing/aggregate/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/aggregate/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/before/Fast.v b/test-suite/coq-makefile/timing/before/Fast.v new file mode 100644 index 0000000000..8b13789179 --- /dev/null +++ b/test-suite/coq-makefile/timing/before/Fast.v @@ -0,0 +1 @@ + diff --git a/test-suite/coq-makefile/timing/before/Slow.v b/test-suite/coq-makefile/timing/before/Slow.v new file mode 100644 index 0000000000..54d3cfc3eb --- /dev/null +++ b/test-suite/coq-makefile/timing/before/Slow.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Definition foo0 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo1 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. +Definition foo2 := Eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl. diff --git a/test-suite/coq-makefile/timing/before/_CoqProject b/test-suite/coq-makefile/timing/before/_CoqProject new file mode 100644 index 0000000000..36c3a18c2b --- /dev/null +++ b/test-suite/coq-makefile/timing/before/_CoqProject @@ -0,0 +1,2 @@ +Slow.v +Fast.v diff --git a/test-suite/coq-makefile/timing/error/A.v b/test-suite/coq-makefile/timing/error/A.v new file mode 100644 index 0000000000..932363a122 --- /dev/null +++ b/test-suite/coq-makefile/timing/error/A.v @@ -0,0 +1 @@ +Check I : I. diff --git a/test-suite/coq-makefile/timing/error/_CoqProject b/test-suite/coq-makefile/timing/error/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/error/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v b/test-suite/coq-makefile/timing/per-file-after/A.v new file mode 100644 index 0000000000..851e2b9738 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/A.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Declare Reduction comp := native_compute. +Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl). +Definition foo1 := Eval comp in (foo0, foo0). diff --git a/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired new file mode 100644 index 0000000000..18f0f34b28 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/A.v.timing.diff.desired @@ -0,0 +1,9 @@ +After | Code | Before || Change | % Change +--------------------------------------------------------------------------------------------------- +0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% +--------------------------------------------------------------------------------------------------- +0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% +0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A +0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97%
\ No newline at end of file diff --git a/test-suite/coq-makefile/timing/per-file-after/_CoqProject b/test-suite/coq-makefile/timing/per-file-after/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-after/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/per-file-before/A.v b/test-suite/coq-makefile/timing/per-file-before/A.v new file mode 100644 index 0000000000..115c1f95bd --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-before/A.v @@ -0,0 +1,4 @@ +Require Coq.ZArith.BinInt. +Declare Reduction comp := vm_compute. +Definition foo0 := Eval comp in (Coq.ZArith.BinInt.Z.div_eucl, Coq.ZArith.BinInt.Z.div_eucl). +Definition foo1 := Eval comp in (foo0, foo0). diff --git a/test-suite/coq-makefile/timing/per-file-before/_CoqProject b/test-suite/coq-makefile/timing/per-file-before/_CoqProject new file mode 100644 index 0000000000..790e057133 --- /dev/null +++ b/test-suite/coq-makefile/timing/per-file-before/_CoqProject @@ -0,0 +1 @@ +A.v diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh new file mode 100755 index 0000000000..9786af10a8 --- /dev/null +++ b/test-suite/coq-makefile/timing/run.sh @@ -0,0 +1,68 @@ +#!/usr/bin/env bash + +#set -x +set -e + +. ../template/init.sh + +cd error +coq_makefile -f _CoqProject -o Makefile +make cleanall +if make pretty-timed TGTS="all" -j1; then + echo "Error: make pretty-timed should have failed" + exit 1 +fi + +cd ../aggregate +coq_makefile -f _CoqProject -o Makefile +make cleanall +make pretty-timed TGTS="all" -j1 || exit $? + +cd ../before +coq_makefile -f _CoqProject -o Makefile +make cleanall +make make-pretty-timed-before TGTS="all" -j1 || exit $? + +cd ../after +coq_makefile -f _CoqProject -o Makefile +make cleanall +make make-pretty-timed-after TGTS="all" -j1 || exit $? +rm -f time-of-build-before.log +make print-pretty-timed-diff TIME_OF_BUILD_BEFORE_FILE=../before/time-of-build-before.log +cp ../before/time-of-build-before.log ./ +make print-pretty-timed-diff || exit $? + +for ext in "" .desired; do + for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + cat ${file}${ext} | grep -v 'warning: undefined variable' | sed s'/[0-9]//g' | sed s'/ *$//g' | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/\(Total.*\)-\(.*\)-/\1+\2+/g' > ${file}${ext}.processed + done +done +for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do + diff -u $file.desired.processed $file.processed || exit $? +done + +cd ../per-file-before +coq_makefile -f _CoqProject -o Makefile +make cleanall +make all TIMING=before -j2 || exit $? + +cd ../per-file-after +coq_makefile -f _CoqProject -o Makefile +make cleanall +make all TIMING=after -j2 || exit $? + +find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';' +make all.timing.diff -j2 || exit $? +cat A.v.timing.diff +echo + +for ext in "" .desired; do + for file in A.v.timing.diff; do + cat ${file}${ext} | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + done +done +for file in A.v.timing.diff; do + diff -u $file.desired.processed $file.processed || exit $? +done + +exit 0 diff --git a/test-suite/coq-makefile/uninstall1/run.sh b/test-suite/coq-makefile/uninstall1/run.sh index e525e12086..5354f794f7 100755 --- a/test-suite/coq-makefile/uninstall1/run.sh +++ b/test-suite/coq-makefile/uninstall1/run.sh @@ -1,11 +1,9 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" @@ -13,7 +11,7 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/uninstall2/run.sh b/test-suite/coq-makefile/uninstall2/run.sh index e525e12086..5354f794f7 100755 --- a/test-suite/coq-makefile/uninstall2/run.sh +++ b/test-suite/coq-makefile/uninstall2/run.sh @@ -1,11 +1,9 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make make html mlihtml make install DSTROOT="$PWD/tmp" @@ -13,7 +11,7 @@ make install-doc DSTROOT="$PWD/tmp" make uninstall DSTROOT="$PWD/tmp" make uninstall-doc DSTROOT="$PWD/tmp" #make debug -(for d in `find tmp -name user-contrib`; do pushd $d >/dev/null; find .; popd >/dev/null; done) | sort -u > actual +(for d in `find tmp -name user-contrib` ; do pushd $d >/dev/null && find . && popd >/dev/null; done) | sort -u > actual sort -u > desired <<EOT . EOT diff --git a/test-suite/coq-makefile/validate1/run.sh b/test-suite/coq-makefile/validate1/run.sh index aaa4194b38..43bf39de10 100755 --- a/test-suite/coq-makefile/validate1/run.sh +++ b/test-suite/coq-makefile/validate1/run.sh @@ -1,10 +1,8 @@ #!/usr/bin/env bash -#set -x -set -e - . ../template/init.sh coq_makefile -f _CoqProject -o Makefile +cat Makefile.conf make exec make validate diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index d91d159d9c..19976b41bd 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index b3fbff680b..1761cc437d 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index c2b521c214..0739982442 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 8db2785837..312dc48bea 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index 8ed3af1ce4..fdd1bddd88 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index 8089de2bf0..b21204b9e4 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index c8dc6303f7..c49dbd7cae 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index 648ab0820c..fae6cd6f3b 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index c8e9af216e..85680e94b9 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh index 1e2afb7540..e07612b84c 100755 --- a/test-suite/misc/deps-checksum.sh +++ b/test-suite/misc/deps-checksum.sh @@ -1,4 +1,4 @@ -rm -f misc/deps/*/*.vo +rm -f misc/deps/A/*.vo misc/deps/B/*.vo $coqc -R misc/deps/A A misc/deps/A/A.v $coqc -R misc/deps/B A misc/deps/B/A.v $coqc -R misc/deps/B A misc/deps/B/B.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 375b706f0a..299f494693 100755 --- a/test-suite/misc/deps-order.sh +++ b/test-suite/misc/deps-order.sh @@ -1,10 +1,10 @@ # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R # See bugs 2242, 2337, 2339 -rm -f misc/deps/*/*.vo +rm -f misc/deps/lib/*.vo misc/deps/client/*.vo tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` $coqdep -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 | head -n 1 > $tmpoutput -diff -u misc/deps/deps.out $tmpoutput 2>&1 +diff -u --strip-trailing-cr misc/deps/deps.out $tmpoutput 2>&1 R=$? times $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 diff --git a/test-suite/modules/polymorphism.v b/test-suite/modules/polymorphism.v new file mode 100644 index 0000000000..63eaa382dc --- /dev/null +++ b/test-suite/modules/polymorphism.v @@ -0,0 +1,81 @@ +Set Universe Polymorphism. + +(** Tests for module subtyping of polymorphic terms *) + +Module Type S. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Parameter foo : Type@{i} -> Type@{j}. + +End Foo. + +End S. + +(** Same constraints *) + +Module OK_1. + +Definition foo@{i j} (A : Type@{i}) : Type@{j} := A. + +End OK_1. + +Module OK_1_Test : S := OK_1. + +(** More general constraints *) + +Module OK_2. + +Inductive X@{i} : Type@{i} :=. +Definition foo@{i j} (A : Type@{i}) : Type@{j} := X@{j}. + +End OK_2. + +Module OK_2_Test : S := OK_2. + +(** Wrong instance length *) + +Module KO_1. + +Definition foo@{i} (A : Type@{i}) : Type@{i} := A. + +End KO_1. + +Fail Module KO_Test_1 : S := KO_1. + +(** Less general constraints *) + +Module KO_2. + +Section Foo. + +Universe i j. +Constraint i < j. + +Definition foo (A : Type@{i}) : Type@{j} := A. + +End Foo. + +End KO_2. + +Fail Module KO_Test_2 : S := KO_2. + +(** Less general constraints *) + +Module KO_3. + +Section Foo. + +Universe i j. +Constraint i = j. + +Definition foo (A : Type@{i}) : Type@{j} := A. + +End Foo. + +End KO_3. + +Fail Module KO_Test_3 : S := KO_3. diff --git a/test-suite/modules/polymorphism2.v b/test-suite/modules/polymorphism2.v new file mode 100644 index 0000000000..7e3327eee0 --- /dev/null +++ b/test-suite/modules/polymorphism2.v @@ -0,0 +1,87 @@ +Set Universe Polymorphism. + +(** Tests for module subtyping of polymorphic terms *) + +Module Type S. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End S. + +(** Same constraints *) + +Module OK_1. + +Section Foo. + +Universes i j. +Constraint i <= j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End OK_1. + +Module OK_1_Test : S := OK_1. + +(** More general constraints *) + +Module OK_2. + +Inductive foo@{i j} : Type@{i} -> Type@{j} :=. + +End OK_2. + +Module OK_2_Test : S := OK_2. + +(** Wrong instance length *) + +Module KO_1. + +Inductive foo@{i} : Type@{i} -> Type@{i} :=. + +End KO_1. + +Fail Module KO_Test_1 : S := KO_1. + +(** Less general constraints *) + +Module KO_2. + +Section Foo. + +Universe i j. +Constraint i < j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End KO_2. + +Fail Module KO_Test_2 : S := KO_2. + +(** Less general constraints *) + +Module KO_3. + +Section Foo. + +Universe i j. +Constraint i = j. + +Inductive foo : Type@{i} -> Type@{j} :=. + +End Foo. + +End KO_3. + +Fail Module KO_Test_3 : S := KO_3. diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 2ccca829d6..b9985a594f 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -1,3 +1,14 @@ +(* Bug 5568, don't warn for notations in repeated module import *) + +Module foo. +Notation compose := (fun g f => g f). +Notation "g & f" := (compose g f) (at level 10). +End foo. + +Import foo. +Import foo. +Import foo. + (**********************************************************************) (* Notations for if and let (submitted by Roland Zumkeller) *) diff --git a/test-suite/output/RecognizePluginWarning.out b/test-suite/output/RecognizePluginWarning.out new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.out diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v new file mode 100644 index 0000000000..cd667bbd00 --- /dev/null +++ b/test-suite/output/RecognizePluginWarning.v @@ -0,0 +1,5 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *) + +(* Test that mentioning a warning defined in plugins works. The failure +mode here is that these result in a warning about unknown warnings, since the +plugins are not known at command line parsing time. *) diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out new file mode 100644 index 0000000000..73369ab713 --- /dev/null +++ b/test-suite/output/TypeclassDebug.out @@ -0,0 +1,18 @@ +Debug: 1: looking for foo without backtracking +Debug: 1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2 : foo +Debug: 1.1-2: looking for foo without backtracking +Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2.1-2 : foo +Debug: 1.1-2.1-2: looking for foo without backtracking +Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2.1-2.1-2 : foo +Debug: 1.1-2.1-2.1-2: looking for foo without backtracking +Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2.1-2.1-2.1-2 : foo +Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking +Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo +The command has indeed failed with message: +Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed. +Tactic failure: Proof search reached its limit. diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v new file mode 100644 index 0000000000..d38e2a50e4 --- /dev/null +++ b/test-suite/output/TypeclassDebug.v @@ -0,0 +1,8 @@ +(* show alternating separators in typeclass debug output; see discussion in PR #868 *) + +Parameter foo : Prop. +Axiom H : foo -> foo. +Hint Resolve H : foo. +Goal foo. +Typeclasses eauto := debug. +Fail typeclasses eauto 5 with foo. diff --git a/test-suite/output/UsePluginWarning.out b/test-suite/output/UsePluginWarning.out new file mode 100644 index 0000000000..47409f3ec5 --- /dev/null +++ b/test-suite/output/UsePluginWarning.out @@ -0,0 +1 @@ +type foo = __ diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v new file mode 100644 index 0000000000..c6e0054641 --- /dev/null +++ b/test-suite/output/UsePluginWarning.v @@ -0,0 +1,7 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) + +Require Extraction. +Axiom foo : Prop. + +Extraction foo. + diff --git a/test-suite/output/Warnings.out b/test-suite/output/Warnings.out new file mode 100644 index 0000000000..a70f8ca45a --- /dev/null +++ b/test-suite/output/Warnings.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-22: +Warning: Projection value has no head constant: fun x : B => x in canonical +instance a of b, ignoring it. [projection-no-head-constant,typechecker] diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v new file mode 100644 index 0000000000..7465442cab --- /dev/null +++ b/test-suite/output/Warnings.v @@ -0,0 +1,5 @@ +(* Term in warning was not printed in the right environment at some time *) +Record A := { B:Type; b:B->B }. +Definition a B := {| B:=B; b:=fun x => x |}. +Canonical Structure a. + diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index f761a4dc5a..73169dae65 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -14,6 +14,7 @@ Definition P (e:option L) := Print P. (* Check that plus is folded even if reduction is involved *) +Set Warnings Append "-deprecated-option". Set Refolding Reduction. Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index e4ee351c3a..0f677a8495 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 438e461357..018b22c489 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/FunindExtraction_compat86.v b/test-suite/success/FunindExtraction_compat86.v new file mode 100644 index 0000000000..8912197d2f --- /dev/null +++ b/test-suite/success/FunindExtraction_compat86.v @@ -0,0 +1,506 @@ +(* -*- coq-prog-args: ("-compat" "8.6") -*- *) + +Definition iszero (n : nat) : bool := + match n with + | O => true + | _ => false + end. + +Functional Scheme iszero_ind := Induction for iszero Sort Prop. + +Lemma toto : forall n : nat, n = 0 -> iszero n = true. +intros x eg. + functional induction iszero x; simpl. +trivial. +inversion eg. +Qed. + + +Function ftest (n m : nat) : nat := + match n with + | O => match m with + | O => 0 + | _ => 1 + end + | S p => 0 + end. +(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *) + +Lemma test1 : forall n m : nat, ftest n m <= 2. +intros n m. + functional induction ftest n m; auto. +Qed. + +Lemma test2 : forall m n, ~ 2 = ftest n m. +Proof. +intros n m;intro H. +functional inversion H ftest. +Qed. + +Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0) \/ n <> 0. +Proof. +functional inversion 1 ftest;auto. +Qed. + + +Require Import Arith. +Lemma test11 : forall m : nat, ftest 0 m <= 2. +intros m. + functional induction ftest 0 m. +auto. +auto. +auto with *. +Qed. + +Function lamfix (m n : nat) {struct n } : nat := + match n with + | O => m + | S p => lamfix m p + end. + +(* Parameter v1 v2 : nat. *) + +Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1. +intros v1 v2. + functional induction lamfix v1 v2. +trivial. +assumption. +Defined. + + + +(* polymorphic function *) +Require Import List. + +Functional Scheme app_ind := Induction for app Sort Prop. + +Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'. +intros A l l'. + functional induction app A l l'; intuition. + rewrite <- H0; trivial. +Qed. + + + + + +Require Export Arith. + + +Function trivfun (n : nat) : nat := + match n with + | O => 0 + | S m => trivfun m + end. + + +(* essaie de parametre variables non locaux:*) + +Parameter varessai : nat. + +Lemma first_try : trivfun varessai = 0. + functional induction trivfun varessai. +trivial. +assumption. +Defined. + + + Functional Scheme triv_ind := Induction for trivfun Sort Prop. + +Lemma bisrepetita : forall n' : nat, trivfun n' = 0. +intros n'. + functional induction trivfun n'. +trivial. +assumption. +Qed. + + + + + + + +Function iseven (n : nat) : bool := + match n with + | O => true + | S (S m) => iseven m + | _ => false + end. + + +Function funex (n : nat) : nat := + match iseven n with + | true => n + | false => match n with + | O => 0 + | S r => funex r + end + end. + + +Function nat_equal_bool (n m : nat) {struct n} : bool := + match n with + | O => match m with + | O => true + | _ => false + end + | S p => match m with + | O => false + | S q => nat_equal_bool p q + end + end. + + +Require Export Div2. +Require Import Nat. +Functional Scheme div2_ind := Induction for div2 Sort Prop. +Lemma div2_inf : forall n : nat, div2 n <= n. +intros n. + functional induction div2 n. +auto. +auto. + +apply le_S. +apply le_n_S. +exact IHn0. +Qed. + +(* reuse this lemma as a scheme:*) + +Function nested_lam (n : nat) : nat -> nat := + match n with + | O => fun m : nat => 0 + | S n' => fun m : nat => m + nested_lam n' m + end. + + +Lemma nest : forall n m : nat, nested_lam n m = n * m. +intros n m. + functional induction nested_lam n m; simpl;auto. +Qed. + + +Function essai (x : nat) (p : nat * nat) {struct x} : nat := + let (n, m) := (p: nat*nat) in + match n with + | O => 0 + | S q => match x with + | O => 1 + | S r => S (essai r (q, m)) + end + end. + +Lemma essai_essai : + forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p. +intros x p. + functional induction essai x p; intros. +inversion H. +auto with arith. + auto with arith. +Qed. + +Function plus_x_not_five'' (n m : nat) {struct n} : nat := + let x := nat_equal_bool m 5 in + let y := 0 in + match n with + | O => y + | S q => + let recapp := plus_x_not_five'' q m in + match x with + | true => S recapp + | false => S recapp + end + end. + +Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. +intros a b. + functional induction plus_x_not_five'' a b; intros hyp; simpl; auto. +Qed. + +Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. +intros n m. + functional induction nat_equal_bool n m; simpl; intros hyp; auto. +rewrite <- hyp in y; simpl in y;tauto. +inversion hyp. +Qed. + +Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. +intros n m. + functional induction nat_equal_bool n m; simpl; intros eg; auto. +inversion eg. +inversion eg. +Qed. + + +Inductive istrue : bool -> Prop := + istrue0 : istrue true. + +Functional Scheme add_ind := Induction for add Sort Prop. + +Lemma inf_x_plusxy' : forall x y : nat, x <= x + y. +intros n m. + functional induction add n m; intros. +auto with arith. +auto with arith. +Qed. + + +Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. +intros n. +unfold plus. + functional induction plus n 0; intros. +auto with arith. +apply le_n_S. +assumption. +Qed. + +Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x. +intros n. + functional induction plus 0 n; intros; auto with arith. +Qed. + +Function mod2 (n : nat) : nat := + match n with + | O => 0 + | S (S m) => S (mod2 m) + | _ => 0 + end. + +Lemma princ_mod2 : forall n : nat, mod2 n <= n. +intros n. + functional induction mod2 n; simpl; auto with arith. +Qed. + +Function isfour (n : nat) : bool := + match n with + | S (S (S (S O))) => true + | _ => false + end. + +Function isononeorfour (n : nat) : bool := + match n with + | S O => true + | S (S (S (S O))) => true + | _ => false + end. + +Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). +intros n. + functional induction isononeorfour n; intros istr; simpl; + inversion istr. +apply istrue0. +destruct n. inversion istr. +destruct n. tauto. +destruct n. inversion istr. +destruct n. inversion istr. +destruct n. tauto. +simpl in *. inversion H0. +Qed. + +Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n). +intros n. + functional induction isononeorfour n; intros m istr; inversion istr. +apply istrue0. +rewrite H in y; simpl in y;tauto. +Qed. + +Function ftest4 (n m : nat) : nat := + match n with + | O => match m with + | O => 0 + | S q => 1 + end + | S p => match m with + | O => 0 + | S r => 1 + end + end. + +Lemma test4 : forall n m : nat, ftest n m <= 2. +intros n m. + functional induction ftest n m; auto with arith. +Qed. + +Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2. +intros n m. +assert ({n0 | n0 = S n}). +exists (S n);reflexivity. +destruct H as [n0 H1]. +rewrite <- H1;revert H1. + functional induction ftest4 n0 m. +inversion 1. +inversion 1. + +auto with arith. +auto with arith. +Qed. + +Function ftest44 (x : nat * nat) (n m : nat) : nat := + let (p, q) := (x: nat*nat) in + match n with + | O => match m with + | O => 0 + | S q => 1 + end + | S p => match m with + | O => 0 + | S r => 1 + end + end. + +Lemma test44 : + forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2. +intros pq n m o r s. + functional induction ftest44 pq n (S m). +auto with arith. +auto with arith. +auto with arith. +auto with arith. +Qed. + +Function ftest2 (n m : nat) {struct n} : nat := + match n with + | O => match m with + | O => 0 + | S q => 0 + end + | S p => ftest2 p m + end. + +Lemma test2' : forall n m : nat, ftest2 n m <= 2. +intros n m. + functional induction ftest2 n m; simpl; intros; auto. +Qed. + +Function ftest3 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match m with + | O => ftest3 p 0 + | S r => 0 + end + end. + +Lemma test3' : forall n m : nat, ftest3 n m <= 2. +intros n m. + functional induction ftest3 n m. +intros. +auto. +intros. +auto. +intros. +simpl. +auto. +Qed. + +Function ftest5 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match m with + | O => ftest5 p 0 + | S r => ftest5 p r + end + end. + +Lemma test5 : forall n m : nat, ftest5 n m <= 2. +intros n m. + functional induction ftest5 n m. +intros. +auto. +intros. +auto. +intros. +simpl. +auto. +Qed. + +Function ftest7 (n : nat) : nat := + match ftest5 n 0 with + | O => 0 + | S r => 0 + end. + +Lemma essai7 : + forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2) + (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) + (n : nat), ftest7 n <= 2. +intros hyp1 hyp2 n. + functional induction ftest7 n; auto. +Qed. + +Function ftest6 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match ftest5 p 0 with + | O => ftest6 p 0 + | S r => ftest6 p r + end + end. + + +Lemma princ6 : + (forall n m : nat, n = 0 -> ftest6 0 m <= 2) -> + (forall n m p : nat, + ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) -> + (forall n m p r : nat, + ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) -> + forall x y : nat, ftest6 x y <= 2. +intros hyp1 hyp2 hyp3 n m. +generalize hyp1 hyp2 hyp3. +clear hyp1 hyp2 hyp3. + functional induction ftest6 n m; auto. +Qed. + +Lemma essai6 : forall n m : nat, ftest6 n m <= 2. +intros n m. + functional induction ftest6 n m; simpl; auto. +Qed. + +(* Some tests with modules *) +Module M. +Function test_m (n:nat) : nat := + match n with + | 0 => 0 + | S n => S (S (test_m n)) + end. + +Lemma test_m_is_double : forall n, div2 (test_m n) = n. +Proof. +intros n. +functional induction (test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. +End M. +(* We redefine a new Function with the same name *) +Function test_m (n:nat) : nat := + pred n. + +Lemma test_m_is_pred : forall n, test_m n = pred n. +Proof. +intro n. +functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*) +reflexivity. +Qed. + +(* Checks if the dot notation are correctly treated in infos *) +Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n. +intro n. +(* here we should apply M.test_m_ind *) +functional induction (M.test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. + +Import M. +(* Now test_m is the one which defines double *) + +Lemma test_m_is_double : forall n, div2 (M.test_m n) = n. +intro n. +(* here we should apply M.test_m_ind *) +functional induction (test_m n). +reflexivity. +simpl;rewrite IHn0;reflexivity. +Qed. + +Extraction iszero. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 1abe14774c..6962e43e7e 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -37,7 +37,6 @@ Hint Resolve predf | 0 : predconv. Goal exists n, pred n. eexists. - Fail Timeout 1 typeclasses eauto with pred. Set Typeclasses Filtered Unification. Set Typeclasses Debug Verbosity 2. (* predf is not tried as it doesn't match the goal *) @@ -80,8 +79,6 @@ Qed. (** The other way around: goal contains redexes instead of instances *) Goal exists n, pred (0 + n). eexists. - (* predf is applied indefinitely *) - Fail Timeout 1 typeclasses eauto with pred. (* pred0 (pred _) matches the goal *) typeclasses eauto with predconv. Qed. @@ -169,8 +166,6 @@ Instance foo f : E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id). Proof. - Fail Timeout 1 apply _. (* 3.7s *) - Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index 767f15be72..bffd96044d 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 023cb5f59d..87296744c4 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/abstract_poly.v b/test-suite/success/abstract_poly.v new file mode 100644 index 0000000000..b736b734fd --- /dev/null +++ b/test-suite/success/abstract_poly.v @@ -0,0 +1,20 @@ +Set Universe Polymorphism. + +Inductive path@{i} {A : Type@{i}} (x : A) : A -> Type@{i} := refl : path x x. +Inductive unit@{i} : Type@{i} := tt. + +Lemma foo@{i j} : forall (m n : unit@{i}) (P : unit -> Type@{j}), path m n -> P m -> P n. +Proof. +intros m n P e p. +abstract (rewrite e in p; exact p). +Defined. + +Check foo_subproof@{Set Set}. + +Lemma bar : forall (m n : unit) (P : unit -> Type), path m n -> P m -> P n. +Proof. +intros m n P e p. +abstract (rewrite e in p; exact p). +Defined. + +Check bar_subproof@{Set Set Set}. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 160f2d9deb..9b0ff1c8fe 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 724e2998ef..055434df01 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 89be144152..4a509da89e 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index c729b23ce7..7e9095dfd7 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 1ed731f50f..35d7929877 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 45c1a5e584..c4c5623897 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index d595cbc2b8..ce1c33fc40 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index 49f20a23f5..37d197a15c 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |