diff options
Diffstat (limited to 'test-suite')
39 files changed, 439 insertions, 26 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 285460762b..e15094ccfa 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 -BIN := $(shell cd ..; readlink -f bin)/ LIB := $(shell cd ..; pwd) +BIN := $(LIB)/bin/ coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite @@ -45,7 +45,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) # read out an emacs config and look for coq-prog-args; if such exists, return it get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1) -get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) +get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist @@ -68,6 +68,7 @@ ifeq (,$(bogomips)) $(warning cannot run complexity tests (no bogomips found)) endif +# keep these synced with test-suite/save-logs.sh log_success = "==========> SUCCESS <==========" log_segfault = "==========> FAILURE <==========" log_anomaly = "==========> FAILURE <==========" @@ -164,7 +165,13 @@ summary.log: $(SHOW) BUILDING SUMMARY FILE $(HIDE)$(MAKE) --quiet summary > "$@" +# if not on travis we can get the log files (they're just there for a +# local build, and downloadable on GitLab) report: summary.log + $(HIDE)./save-logs.sh + $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:start:coq.logs'; fi + $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec cat '{}' ';'; fi + $(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:end:coq.logs'; fi $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v new file mode 100644 index 0000000000..806ffb771f --- /dev/null +++ b/test-suite/bugs/closed/4132.v @@ -0,0 +1,31 @@ + +Require Import ZArith Omega. +Open Scope Z_scope. + +(** bug 4132: omega was using "simpl" either on whole equations, or on + delimited but wrong spots. This was leading to unexpected reductions + when one atom (here [b]) is an evaluable reference instead of a variable. *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) +Qed. + +Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "index out of bounds" in the past, + but I never managed to reproduce that in any version, + even before my fix. *) +Qed. + +Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "Failure(occurence 2)" in the past, + but I never managed to reproduce that. *) +Qed. diff --git a/test-suite/bugs/closed/5019.v b/test-suite/bugs/closed/5019.v new file mode 100644 index 0000000000..7c973f88b5 --- /dev/null +++ b/test-suite/bugs/closed/5019.v @@ -0,0 +1,5 @@ +Require Import Coq.ZArith.ZArith. +Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. + clear; intros. + Timeout 1 zify. (* used to loop forever; should take < 0.01 s *) +Admitted. diff --git a/test-suite/bugs/closed/5233.v b/test-suite/bugs/closed/5233.v new file mode 100644 index 0000000000..06286c740d --- /dev/null +++ b/test-suite/bugs/closed/5233.v @@ -0,0 +1,2 @@ +(* Implicit arguments on type were missing for recursive records *) +Inductive foo {A : Type} : Type := { Foo : foo }. diff --git a/test-suite/bugs/closed/5255.v b/test-suite/bugs/closed/5255.v new file mode 100644 index 0000000000..5daaf9edbf --- /dev/null +++ b/test-suite/bugs/closed/5255.v @@ -0,0 +1,24 @@ +Section foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End foo. + +Module Type Foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End Foo. + +Set Universe Polymorphism. + +Inductive unit := tt. +Inductive eq {A} (x y : A) : Type := eq_refl : eq x y. + +Section bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End bar. + +Module Type Bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End Bar. diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v new file mode 100644 index 0000000000..390133162f --- /dev/null +++ b/test-suite/bugs/closed/5486.v @@ -0,0 +1,15 @@ +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k : + forall _ : T, Fm), + @eq Fm + (k + match p return T with + | pair p0 swap => fst p0 + end) f. + intros. + (* next statement failed in Bug 5486 *) + match goal with + | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ] + => pose (let (a, b) := d in e a b) as t0 + end. diff --git a/test-suite/bugs/closed/5523.v b/test-suite/bugs/closed/5523.v new file mode 100644 index 0000000000..d7582a3797 --- /dev/null +++ b/test-suite/bugs/closed/5523.v @@ -0,0 +1,6 @@ +(* Support for complex constructions in recursive notations, especially "match". *) + +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. +Notation "'dlet' x , y := v 'in' ( a , b , .. , c )" + := (Let_In v (fun '(x, y) => pair .. (pair a b) .. c)) + (at level 0). diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v new file mode 100644 index 0000000000..88f219be30 --- /dev/null +++ b/test-suite/bugs/closed/5526.v @@ -0,0 +1,3 @@ +Fail Notation "x === x" := (eq_refl x) (at level 10). +Reserved Notation "x === x" (only printing, at level 10). +Notation "x === x" := (eq_refl x) (only printing). diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v new file mode 100644 index 0000000000..bb1222489a --- /dev/null +++ b/test-suite/bugs/closed/5550.v @@ -0,0 +1,10 @@ +Section foo. + + Variable bar : Prop. + Variable H : bar. + + Goal bar. + typeclasses eauto with foobar. + Qed. + +End foo. diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh index da84067d51..9f6295d644 100755 --- a/test-suite/coq-makefile/native1/run.sh +++ b/test-suite/coq-makefile/native1/run.sh @@ -3,7 +3,8 @@ #set -x set -e -if which ocamlopt; then +NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true +if [[ `which ocamlopt` && $NATIVECOMP ]]; then . ../template/init.sh 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 new file mode 100755 index 0000000000..6301aa03c0 --- /dev/null +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -0,0 +1,37 @@ +#!/usr/bin/env bash + +set -e + +git clean -dfx + +cat > _CoqProject <<EOT +-I src/ + +./src/test_plugin.mllib +./src/test.ml4 +./src/test.mli +EOT + +mkdir src + +cat > src/test_plugin.mllib <<EOT +Test +EOT + +touch src/test.mli + +cat > src/test.ml4 <<EOT +DECLARE PLUGIN "test" + +let _ = Pre_env.empty_env +EOT + +${COQBIN}coq_makefile -f _CoqProject -o Makefile + +if make VERBOSE=1; then + # make command should have failed (but didn't) + exit 1 +else + # make command should have failed (and it indeed did) + exit 0 +fi 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 new file mode 100755 index 0000000000..991fb4a61d --- /dev/null +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh @@ -0,0 +1,32 @@ +#!/usr/bin/env bash + +set -e + +git clean -dfx + +cat > _CoqProject <<EOT +-bypass-API +-I src/ + +./src/test_plugin.mllib +./src/test.ml4 +./src/test.mli +EOT + +mkdir src + +cat > src/test_plugin.mllib <<EOT +Test +EOT + +touch src/test.mli + +cat > src/test.ml4 <<EOT +DECLARE PLUGIN "test" + +let _ = Pre_env.empty_env +EOT + +${COQBIN}coq_makefile -f _CoqProject -o Makefile + +make VERBOSE=1 diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.ml4 index 72765abe04..e7d0bfe1f8 100644 --- a/test-suite/coq-makefile/template/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.ml4 @@ -1,3 +1,4 @@ +open API open Ltac_plugin DECLARE PLUGIN "test_plugin" let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; diff --git a/test-suite/coq-makefile/template/src/test_aux.ml b/test-suite/coq-makefile/template/src/test_aux.ml index a01d0865a8..e134abd840 100644 --- a/test-suite/coq-makefile/template/src/test_aux.ml +++ b/test-suite/coq-makefile/template/src/test_aux.ml @@ -1 +1 @@ -let tac = Proofview.tclUNIT () +let tac = API.Proofview.tclUNIT () diff --git a/test-suite/coq-makefile/template/src/test_aux.mli b/test-suite/coq-makefile/template/src/test_aux.mli index 10020f27de..2e7ad1529f 100644 --- a/test-suite/coq-makefile/template/src/test_aux.mli +++ b/test-suite/coq-makefile/template/src/test_aux.mli @@ -1 +1 @@ -val tac : unit Proofview.tactic +val tac : unit API.Proofview.tactic diff --git a/test-suite/coqchk/univ.v b/test-suite/coqchk/univ.v index 84a4009d7e..19eea94b19 100644 --- a/test-suite/coqchk/univ.v +++ b/test-suite/coqchk/univ.v @@ -33,3 +33,16 @@ Inductive finite_of_order T (D : T -> Type) (n : natural) := (rank_injective : injective_in T natural D rank) (rank_onto : forall i, equivalent (less_than i n) (in_image T natural D rank i)). + +(* Constraints *) +Universes i j. +Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})). +Constraint i < j. +Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}). +Universes i' j'. +Constraint i' = j'. +Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})). +Inductive constraint4 : (Type -> Type) -> Type + := mk_constraint4 : let U1 := Type in + let U2 := Type in + constraint4 (fun x : U1 => (x : U2)). diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 8ce6f9795c..f064dfe763 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -2,18 +2,18 @@ t_rect = fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with - | @k _ x0 => f x0 (F x0) + | k _ x0 => f x0 (F x0) end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t Argument scopes are [function_scope function_scope _] = fun d : TT => match d with - | @CTT _ _ b => b + | {| f3 := b |} => b end : TT -> 0 = 0 = fun d : TT => match d with - | @CTT _ _ b => b + | {| f3 := b |} => b end : TT -> 0 = 0 proj = @@ -72,3 +72,11 @@ e1 : texp t1 e2 : texp t2 The term "0" has type "nat" while it is expected to have type "typeDenote t0". +fun '{{n, m, _}} => n + m + : J -> nat +fun '{{n, m, p}} => n + m + p + : J -> nat +fun '(D n m p q) => n + m + p + q + : J -> nat +The command has indeed failed with message: +The constructor D (in type J) expects 3 arguments. diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4074896420..6a4fd007df 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -106,3 +106,18 @@ Fail Fixpoint texpDenote t (e:texp t):typeDenote t:= | TBinop t1 t2 _ b e1 e2 => O end. +(* Test notations with local definitions in constructors *) + +Inductive J := D : forall n m, let p := n+m in nat -> J. +Notation "{{ n , m , q }}" := (D n m q). + +Check fun x : J => let '{{n, m, _}} := x in n + m. +Check fun x : J => let '{{n, m, p}} := x in n + m + p. + +(* Cannot use the notation because of the dependency in p *) + +Check fun x => let '(D n m p q) := x in n+m+p+q. + +(* This used to succeed, being interpreted as "let '{{n, m, p}} := ..." *) + +Fail Check fun x : J => let '{{n, m, _}} p := x in n + m + p. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 4d59a92cbf..ffea0819a5 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -98,5 +98,14 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) : nat -> Prop tele (t : Type) '(y, z) (x : t0) := tt : forall t : Type, nat * nat -> t -> fpack +[fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2] + : (nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * + ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat)))))) foo5 x nat x : nat -> nat +fun x : ?A => x === x + : forall x : ?A, x = x +where +?A : [x : ?A |- Type] (x cannot be used) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 96d831944f..250aecafd4 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -140,7 +140,23 @@ Notation "'tele' x .. z := b" := Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. +(* Checking that "fun" in a notation does not mixed up with the + detection of a recursive binder *) + +Notation "[ x ;; .. ;; y ]" := ((x,((fun u => S u), .. (y,(fun u => S u,fun v:nat => v)) ..))). +Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ]. + (* Cyprien's part of bug #4765 *) +Section Bug4765. + Notation foo5 x T y := (fun x : T => y). Check foo5 x nat x. + +End Bug4765. + +(**********************************************************************) +(* Test printing of #5526 *) + +Notation "x === x" := (eq_refl x) (only printing, at level 10). +Check (fun x => eq_refl x). diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index 36d643a447..d45343fe60 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -14,3 +14,19 @@ build 5 : test_r build_c 5 : test_c +fun '(C _ p) => p + : N -> True +fun '{| T := T |} => T + : N -> Type +fun '(C T p) => (T, p) + : N -> Type * True +fun '{| q := p |} => p + : M -> True +fun '{| U := T |} => T + : M -> Type +fun '{| U := T; q := p |} => (T, p) + : M -> Type * True +fun '{| U := T; a := a; q := p |} => (T, p, a) + : M -> Type * True * nat +fun '{| U := T; a := a; q := p |} => (T, p, a) + : M -> Type * True * nat diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 6aa3df9830..d9a649fadc 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -19,3 +19,15 @@ Check build 5. Check {| field := 5 |}. Check build_r 5. Check build_c 5. + +Record N := C { T : Type; _ : True }. +Check fun x:N => let 'C _ p := x in p. +Check fun x:N => let 'C T _ := x in T. +Check fun x:N => let 'C T p := x in (T,p). + +Record M := D { U : Type; a := 0; q : True }. +Check fun x:M => let 'D T _ p := x in p. +Check fun x:M => let 'D T _ p := x in T. +Check fun x:M => let 'D T p := x in (T,p). +Check fun x:M => let 'D T a p := x in (T,p,a). +Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a). diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out index bf1bf2809d..ca56f032ff 100644 --- a/test-suite/output/Show.out +++ b/test-suite/output/Show.out @@ -1,12 +1,10 @@ -3 subgoals (ID 29) +3 subgoals (ID 31) H : 0 = 0 ============================ 1 = 1 -subgoal 2 (ID 33) is: +subgoal 2 (ID 35) is: 1 = S (S m') -subgoal 3 (ID 20) is: +subgoal 3 (ID 22) is: S (S n') = S m - -(dependent evars: (printing disabled) ) diff --git a/test-suite/output/ShowMatch.out b/test-suite/output/ShowMatch.out new file mode 100644 index 0000000000..e5520b8dfa --- /dev/null +++ b/test-suite/output/ShowMatch.out @@ -0,0 +1,8 @@ +match # with + | f => + end + +match # with + | A.f => + end + diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v new file mode 100644 index 0000000000..02b7eada83 --- /dev/null +++ b/test-suite/output/ShowMatch.v @@ -0,0 +1,13 @@ +(* Bug 5546 complained about unqualified constructors in Show Match output, + when qualification is needed to disambiguate them +*) + +Module A. + Inductive foo := f. + Show Match foo. (* no need to disambiguate *) +End A. + +Module B. + Inductive foo := f. + (* local foo shadows A.foo, so constructor "f" needs disambiguation *) + Show Match A.foo. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index c70467912f..d28ee42761 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,13 +6,13 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x : T n := A n in ?t ?y : T n +fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where -?t : [n : nat x := A n : T n |- ?T -> T n] -?y : [n : nat x := A n : T n |- ?T] -fun n : nat => ?t ?y : T n +?t : [n : nat y := A n : T n |- ?T -> T n] +?x : [n : nat y := A n : T n |- ?T] +fun n : nat => ?t ?x : T n : forall n : nat, T n where ?t : [n : nat |- ?T -> T n] -?y : [n : nat |- ?T] +?x : [n : nat |- ?T] diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v index 1825db1676..f761a4dc5a 100644 --- a/test-suite/output/inference.v +++ b/test-suite/output/inference.v @@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H). (* Note: exact numbers of evars are not important... *) Inductive T (n:nat) : Type := A : T n. -Check fun n (x:=A n:T n) => _ _ : T n. +Check fun n (y:=A n:T n) => _ _ : T n. Check fun n => _ _ : T n. diff --git a/test-suite/output/names.out b/test-suite/output/names.out index 9471b892dd..48be63a46a 100644 --- a/test-suite/output/names.out +++ b/test-suite/output/names.out @@ -3,3 +3,9 @@ In environment y : nat The term "a y" has type "{y0 : nat | y = y0}" while it is expected to have type "{x : nat | x = y}". +1 focused subgoal +(shelved: 1) + + H : ?n <= 3 -> 3 <= ?n -> ?n = 3 + ============================ + True diff --git a/test-suite/output/names.v b/test-suite/output/names.v index b3b5071a03..f1efd0df2a 100644 --- a/test-suite/output/names.v +++ b/test-suite/output/names.v @@ -3,3 +3,7 @@ Parameter a : forall x, {y:nat|x=y}. Fail Definition b y : {x:nat|x=y} := a y. + +Goal (forall n m, n <= m -> m <= n -> n = m) -> True. +intro H; epose proof (H _ 3) as H. +Show. diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh new file mode 100755 index 0000000000..b613621085 --- /dev/null +++ b/test-suite/save-logs.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash + +SAVEDIR="logs" + +# reset for local builds +rm -rf "$SAVEDIR" +mkdir "$SAVEDIR" + +# keep this synced with test-suite/Makefile +FAILMARK="==========> FAILURE <==========" + +FAILED=$(mktemp /tmp/coq-check-XXXXX) +find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" + +rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" +cp summary.log "$SAVEDIR"/ + +# cleanup +rm "$FAILED" diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index ffd50f6efd..69dc9aca78 100644 --- a/test-suite/success/Abstract.v +++ b/test-suite/success/Abstract.v @@ -1,4 +1,3 @@ - (* Cf coqbugs #546 *) Require Import Omega. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index f07773f8bd..921433cadd 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -27,3 +27,8 @@ Parameters (a:_) (b:a=0). Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl. Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat. + +(* Some example which should succeed with local implicit arguments *) + +Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A. +Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P. diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 8334322c99..6f27c1d369 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -87,3 +87,8 @@ Record R : Type := { P (A : Type) : Prop := exists x : A -> A, x = x; Q A : P A -> P A }. + +(* We allow reusing an implicit parameter named in non-recursive types *) +(* This is used in a couple of development such as UniMatch *) + +Record S {A:Type} := { a : A; b : forall A:Type, A }. diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 43e3493c1e..ca37467166 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -20,3 +20,9 @@ Inductive U := A. Bind Scope u with U. Notation "'ε'" := A : u. Definition c := ε : U. + +(* Check activation of type scope for tactics such as assert *) + +Goal True. +assert (nat * nat). + diff --git a/test-suite/success/cbn.v b/test-suite/success/cbn.v new file mode 100644 index 0000000000..6aeb05f54e --- /dev/null +++ b/test-suite/success/cbn.v @@ -0,0 +1,18 @@ +(* cbn is able to refold mutual recursive calls *) + +Fixpoint foo (n : nat) := + match n with + | 0 => true + | S n => g n + end +with g (n : nat) : bool := + match n with + | 0 => true + | S n => foo n + end. +Goal forall n, foo (S n) = g n. + intros. cbn. + match goal with + |- g _ = g _ => reflexivity + end. +Qed.
\ No newline at end of file diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v index 5b9265b6a8..05ab913932 100644 --- a/test-suite/success/coindprim.v +++ b/test-suite/success/coindprim.v @@ -13,9 +13,10 @@ Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}. CoFixpoint ones := {| hd := 1; tl := ones |}. CoFixpoint ticks := {| hd := tt; tl := ticks |}. -CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop := - mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }. -Arguments stream_equiv {A} s s'. +CoInductive stream_equiv {A} (s : Stream A) (s' : Stream A) : Prop := + mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv s.(tl) s'.(tl) }. +Arguments hdeq {A} {s} {s'}. +Arguments tleq {A} {s} {s'}. Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) := {| hdeq := eq_refl; tleq := ones_eq |}. @@ -88,4 +89,4 @@ Lemma eq (x : U) : x = force x. Proof. Fail destruct x. Abort. - (* Impossible *)
\ No newline at end of file + (* Impossible *) diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 4e2bf45118..c36313ec16 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -62,7 +62,7 @@ Check Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))). -(* This used to fail with anomaly (Pp.str "evar was not declared") in V8.0pl3 *) +(* This used to fail with anomaly (Pp.str "evar was not declared.") in V8.0pl3 *) Theorem contradiction : forall p, ~ p -> p -> False. Proof. trivial. Qed. @@ -414,4 +414,10 @@ Axiom test : forall P1 P2, P1 = P2 -> P1 -> P2. Import EqNotations. Definition test2 {A B:Type} {H:A=B} (a:A) : B := rew H in a. +(* Check that pre-existing evars are not counted as newly undefined in "set" *) +(* Reported by Théo *) +Goal exists n : nat, n = n -> True. +eexists. +set (H := _ = _). +Abort. diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v new file mode 100644 index 0000000000..0ed5b524f3 --- /dev/null +++ b/test-suite/success/forward.v @@ -0,0 +1,18 @@ +(* Testing forward reasoning *) + +Goal 0=0. +Fail assert (_ = _). +eassert (_ = _)by reflexivity. +eassumption. +Qed. + +Goal 0=0. +Fail set (S ?[nl]). +eset (S ?[n]). +remember (S ?n) as x. +instantiate (n:=0). +Fail remember (S (S _)). +eremember (S (S ?[x])). +instantiate (x:=0). +reflexivity. +Qed. diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 4b41a509e5..f12db8b081 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -17,6 +17,29 @@ specialize (eq_trans (x:=a)(y:=b)). intros _. specialize (eq_trans H H0). intros _. specialize (eq_trans H0 (z:=b)). intros _. +(* incomplete bindings: y is left quantified and z is instantiated. *) +specialize eq_trans with (x:=a)(z:=c). +intro h. +(* y can be instantiated now *) +specialize h with (y:=b). +(* z was instantiated above so this must fail. *) +Fail specialize h with (z:=c). +clear h. + +(* incomplete bindings: 1st dep hyp is instantiated thus A, x and y + instantiated too. *) +specialize eq_trans with (1:=H). +intro h. +(* 2nd dep hyp can be instantiated now, which instatiates z too. *) +specialize h with (1:=H0). +(* checking that there is no more products in h. *) +match type of h with +| _ = _ => idtac +| _ => fail "specialize test failed: hypothesis h should be an equality at this point" +end. +clear h. + + (* local "in place" specialization *) assert (Eq:=eq_trans). @@ -31,6 +54,27 @@ specialize (Eq _ a b c). Undo. specialize (Eq _ _ _ _ H H0). Undo. specialize (Eq _ _ _ b H0). Undo. +(* incomplete binding *) +specialize Eq with (y:=b). +(* A and y have been instantiated so this works *) +specialize (Eq _ _ H H0). +Undo 2. + +(* incomplete binding (dependent) *) +specialize Eq with (1:=H). +(* A, x and y have been instantiated so this works *) +specialize (Eq _ H0). +Undo 2. + +(* incomplete binding (dependent) *) +specialize Eq with (1:=H) (2:=H0). +(* A, x and y have been instantiated so this works *) +match type of Eq with +| _ = _ => idtac +| _ => fail "specialize test failed: hypothesis Eq should be an equality at this point" +end. +Undo 2. + (* (** strange behavior to inspect more precisely *) @@ -40,7 +84,7 @@ specialize (Eq _ _ _ b H0). Undo. (* 2) echoue moins lorsque zero premise de mangé *) specialize eq_trans with (1:=Eq). (* mal typé !! *) -(* 3) *) +(* 3) Seems fixed.*) specialize eq_trans with _ a b c. intros _. (* Anomaly: Evar ?88 was not declared. Please report. *) *) |