diff options
Diffstat (limited to 'test-suite')
24 files changed, 94 insertions, 55 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v index 3e3a987a7c..b80e0bb0e4 100644 --- a/test-suite/bugs/closed/HoTT_coq_056.v +++ b/test-suite/bugs/closed/HoTT_coq_056.v @@ -94,9 +94,9 @@ Definition FunctorApplicationOf {C D} F {argsT} args {T} {rtn} Global Arguments FunctorApplicationOf / {C} {D} F {argsT} args {T} {rtn} {_}. Global Instance FunctorApplicationDash C D (F : Functor C D) -: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0. +: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0 := {}. Global Instance FunctorApplicationFunctorFunctor' A B C C' D (F : Functor (A * B) D) (G : Functor C A) (H : Functor C' B) -: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100. +: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100 := {}. Notation "F ⟨ x ⟩" := (FunctorApplicationOf F%functor x%functor) : functor_scope. diff --git a/test-suite/bugs/closed/bug_3324.v b/test-suite/bugs/closed/bug_3324.v index 45dbb57aa2..dae0d4c024 100644 --- a/test-suite/bugs/closed/bug_3324.v +++ b/test-suite/bugs/closed/bug_3324.v @@ -6,7 +6,7 @@ Module ETassi. Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}. Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. Canonical Structure default_HSet:= fun T P => (@BuildhSet T P). - Global Instance isset_hProp : IsHSet hProp | 0. + Global Instance isset_hProp : IsHSet hProp | 0 := {}. Check (eq_refl _ : setT (default_HSet _ _) = hProp). Check (eq_refl _ : setT _ = hProp). @@ -22,7 +22,7 @@ Module JGross. Definition Unit_hp:hProp:=(hp Unit admit). Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}. Canonical Structure default_HSet:= fun T P => (@BuildhSet T P). - Global Instance isset_hProp : IsHSet hProp | 0. + Global Instance isset_hProp : IsHSet hProp | 0 := {}. Definition isepi {X Y} `(f:X->Y) := forall Z: hSet, forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h. Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> True. diff --git a/test-suite/bugs/closed/bug_3454.v b/test-suite/bugs/closed/bug_3454.v index e4cd60cb24..0a01adec33 100644 --- a/test-suite/bugs/closed/bug_3454.v +++ b/test-suite/bugs/closed/bug_3454.v @@ -32,14 +32,14 @@ Local Instance isequiv_tgt_compose A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) (@compose A {xy : B * B & fst xy = snd xy} B - (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)). + (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)) := {}. (* Toplevel input, characters 220-223: *) (* Error: Cannot infer this placeholder. *) Local Instance isequiv_tgt_compose' A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) - (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)). + (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)) := {}. (* Toplevel input, characters 221-232: *) (* Error: *) (* In environment *) @@ -52,7 +52,7 @@ Local Instance isequiv_tgt_compose'' A B : @IsEquiv (A -> {xy : B * B & fst xy = snd xy}) (A -> B) (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) - (fun s => s.(projT1)))). + (fun s => s.(projT1)))) := {}. (* Toplevel input, characters 15-241: Error: Cannot infer an internal placeholder of type "Type" in environment: diff --git a/test-suite/bugs/closed/bug_3682.v b/test-suite/bugs/closed/bug_3682.v index 9d37d1a2d0..07b759afb5 100644 --- a/test-suite/bugs/closed/bug_3682.v +++ b/test-suite/bugs/closed/bug_3682.v @@ -1,6 +1,6 @@ Require Import TestSuite.admit. Class Foo. Definition bar `{Foo} (x : Set) := Set. -Instance: Foo. +Instance: Foo := {}. Definition bar1 := bar nat. Definition bar2 := bar ltac:(admit). diff --git a/test-suite/bugs/closed/bug_4782.v b/test-suite/bugs/closed/bug_4782.v index be17a96f15..c08195d502 100644 --- a/test-suite/bugs/closed/bug_4782.v +++ b/test-suite/bugs/closed/bug_4782.v @@ -15,8 +15,8 @@ Record T := { dom : Type }. Definition pairT A B := {| dom := (dom A * dom B)%type |}. Class C (A:Type). Parameter B:T. -Instance c (A:T) : C (dom A). -Instance cn : C (dom B). +Instance c (A:T) : C (dom A) := {}. +Instance cn : C (dom B) := {}. Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A. Set Typeclasses Debug. Goal forall (A:T) (x:dom A), pairT A A = pairT A A. diff --git a/test-suite/bugs/closed/bug_4798.v b/test-suite/bugs/closed/bug_4798.v index 41a1251ca5..696812dee1 100644 --- a/test-suite/bugs/closed/bug_4798.v +++ b/test-suite/bugs/closed/bug_4798.v @@ -1,3 +1,5 @@ +(* 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.7"). Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/bug_5401.v b/test-suite/bugs/closed/bug_5401.v index 95193b993b..466e669d00 100644 --- a/test-suite/bugs/closed/bug_5401.v +++ b/test-suite/bugs/closed/bug_5401.v @@ -5,7 +5,7 @@ Parameter P : nat -> Type. Parameter v : forall m, P m. Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0. Class U (R : P 0) (m : forall x, P x) : Prop. -Instance w : U (f _ (fun _ => v _)) v. +Instance w : U (f _ (fun _ => v _)) v := {}. Print HintDb typeclass_instances. End A. diff --git a/test-suite/bugs/closed/bug_9166.v b/test-suite/bugs/closed/bug_9166.v index 8a7e9c37b0..a89837dd12 100644 --- a/test-suite/bugs/closed/bug_9166.v +++ b/test-suite/bugs/closed/bug_9166.v @@ -1,3 +1,5 @@ +(* DO NOT MODIFY THIS FILE DIRECTLY *) +(* It is autogenerated by dev/tools/update-compat.py. *) Set Warnings "+deprecated". Notation bar := option (compat "8.7"). diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake new file mode 100644 index 0000000000..aa68fad39e --- /dev/null +++ b/test-suite/ide/debug_ltac.fake @@ -0,0 +1,2 @@ +FAILADD { Debug On. } +ADD { Set Debug On. } diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 94016e170b..72d5a9253a 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -45,5 +45,9 @@ fun x : nat => (x.-1)%pred : Prop ## : Prop +myAnd1 True True + : Prop +r 2 3 + : Prop Notation Cn := Foo.FooCn Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 309115848f..90babf9c55 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -165,6 +165,22 @@ Check ##. End H. +(* Fixing bugs reported by G. Gonthier in #9207 *) + +Module I. + +Definition myAnd A B := A /\ B. +Notation myAnd1 A := (myAnd A). +Check myAnd1 True True. + +Set Warnings "-auto-template". + +Record Pnat := {inPnat :> nat -> Prop}. +Axiom r : nat -> Pnat. +Check r 2 3. + +End I. + (* Fixing a bug reported by G. Gonthier in #9207 *) Module J. diff --git a/test-suite/report.sh b/test-suite/report.sh index cef615266b..71aac029ea 100755 --- a/test-suite/report.sh +++ b/test-suite/report.sh @@ -24,21 +24,11 @@ cp summary.log "$SAVEDIR"/ rm "$FAILED" # print info -if [ -n "$TRAVIS" ] || [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then +if [ -n "$APPVEYOR" ] || [ -n "$PRINT_LOGS" ]; then find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do - if [ -n "$TRAVIS" ]; then - # ${foo////.} replaces every / by . in $foo - printf 'travis_fold:start:coq.logs.%s\n' "${file////.}"; - else printf '%s\n' "$file" - fi - + printf '%s\n' "$file" cat "$file" - - if [ -n "$TRAVIS" ]; then - # ${foo////.} replaces every / by . in $foo - printf 'travis_fold:end:coq.logs.%s\n' "${file////.}"; - else printf '\n' - fi + printf '\n' done printed_logs=1 fi diff --git a/test-suite/ssr/ipat_replace.v b/test-suite/ssr/ipat_replace.v new file mode 100644 index 0000000000..528f33f30d --- /dev/null +++ b/test-suite/ssr/ipat_replace.v @@ -0,0 +1,17 @@ +Require Import ssreflect. + +Lemma test : True. +Proof. +have H : True. + by []. +have {}H : True. + by apply: H. +by apply: H. +Qed. + +Lemma test2 (H : True) : False -> False -> False. +Proof. +move=> {}W. +move=> {}H. +by apply: H. +Qed. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 5650dba236..81469d79c3 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq89. +Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index 37d50ee67d..afeb57f9f2 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.7") -*- *) +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq810. Import Coq.Compat.Coq89. Import Coq.Compat.Coq88. -Import Coq.Compat.Coq87. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..1f62635f50 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.7") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq810. +Import Coq.Compat.Coq89. +Import Coq.Compat.Coq88. +Import Coq.Compat.Coq87. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 9981388381..c8f75915c8 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(* -*- coq-prog-args: ("-compat" "8.9") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq810. Import Coq.Compat.Coq89. -Import Coq.Compat.Coq88. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 9086621344..3888cafed3 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -14,7 +14,7 @@ Module onlyclasses. Module RJung. Class Foo (x : nat). - Instance foo x : x = 2 -> Foo x. + Instance foo x : x = 2 -> Foo x := {}. Hint Extern 0 (_ = _) => reflexivity : typeclass_instances. Typeclasses eauto := debug. Check (_ : Foo 2). @@ -63,7 +63,7 @@ End RefineVsNoTceauto. Module Leivantex2PR339. (** Was a bug preventing to find hints associated with no pattern *) Class Bar := {}. - Instance bar1 (t:Type) : Bar. + Instance bar1 (t:Type) : Bar := {}. Hint Extern 0 => exact True : typeclass_instances. Typeclasses eauto := debug. Goal Bar. @@ -222,10 +222,10 @@ Module IterativeDeepening. Class B. Class C. - Instance: B -> A | 0. - Instance: C -> A | 0. - Instance: C -> B -> A | 0. - Instance: A -> A | 0. + Instance: B -> A | 0 := {}. + Instance: C -> A | 0 := {}. + Instance: C -> B -> A | 0 := {}. + Instance: A -> A | 0 := {}. Goal C -> A. intros. diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index 5477c83316..62a66daf7d 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -51,7 +51,7 @@ Qed. Class B (A : Type). Class I. -Instance i : I. +Instance i : I := {}. Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y. Class D (f : nat -> nat -> nat). @@ -59,7 +59,7 @@ Definition ftest (x y : nat) := x + y. Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f). Admitted. Module Instnopat. - Local Instance: B nat. + Local Instance: B nat := {}. (* pattern_of_constr -> B nat *) (* exact hint *) Check (_ : B nat). @@ -72,7 +72,7 @@ Module Instnopat. eauto with typeclass_instances. Qed. - Local Instance: D ftest. + Local Instance: D ftest := {}. Local Hint Resolve flipD | 0 : typeclass_instances. (* pattern: D (flip _) *) Fail Timeout 1 Check (_ : D _). (* loops applying flipD *) @@ -80,7 +80,7 @@ Module Instnopat. End Instnopat. Module InstnopatApply. - Local Instance: I -> B nat. + Local Instance: I -> B nat := {}. (* pattern_of_constr -> B nat *) (* apply hint *) Check (_ : B nat). @@ -116,7 +116,7 @@ Module InstPat. Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances. Module withftest. - Local Instance: D ftest. + Local Instance: D ftest := {}. Check (_ : D _). (* D_instance_0 : D ftest *) diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 730b367d60..cea7d92c0b 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -149,10 +149,10 @@ Module IterativeDeepening. Class B. Class C. - Instance: B -> A | 0. - Instance: C -> A | 0. - Instance: C -> B -> A | 0. - Instance: A -> A | 0. + Instance: B -> A | 0 := {}. + Instance: C -> A | 0 := {}. + Instance: C -> B -> A | 0 := {}. + Instance: A -> A | 0 := {}. Goal C -> A. intros. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index d1d384659b..573912c7cd 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -263,7 +263,7 @@ Abort. (* This one was working in 8.4 (because of full conv on closed arguments) *) Class E. -Instance a:E. +Instance a:E := {}. Goal forall h : E -> nat -> nat, h (id a) 0 = h a 0. intros. destruct (h _). diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index c44747379f..5b616ccc33 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -9,11 +9,11 @@ (************************************************************************) Class A (A : Type). - Instance an: A nat. + Instance an: A nat := {}. Class B (A : Type) (a : A). -Instance bn0: B nat 0. -Instance bn1: B nat 1. +Instance bn0: B nat 0 := {}. +Instance bn1: B nat 1 := {}. Goal A nat. Proof. @@ -39,7 +39,7 @@ Proof. eexists. eexists. typeclasses eauto. Defined. -Instance ab: A bool. (* Backtrack on A instance *) +Instance ab: A bool := {}. (* Backtrack on A instance *) Goal exists (T : Type) (t : T), A T /\ B T t. Proof. eexists. eexists. typeclasses eauto. @@ -51,7 +51,7 @@ Hint Extern 0 { x : ?A & _ } => unshelve class_apply @existT : typeclass_instances. Existing Class sigT. Set Typeclasses Debug. -Instance can: C an 0. +Instance can: C an 0 := {}. (* Backtrack on instance implementation *) Goal exists (T : Type) (t : T), { x : A T & C x t }. Proof. @@ -59,7 +59,7 @@ Proof. Defined. Class D T `(a: A T). - Instance: D _ an. + Instance: D _ an := {}. Goal exists (T : Type), { x : A T & D T x }. Proof. eexists. typeclasses eauto. diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index 79467e549c..351481b0b6 100644 --- a/test-suite/success/setoid_test2.v +++ b/test-suite/success/setoid_test2.v @@ -120,7 +120,7 @@ Axiom eqS1: S1 -> S1 -> Prop. Axiom SetoidS1 : Setoid_Theory S1 eqS1. Add Setoid S1 eqS1 SetoidS1 as S1setoid. -Instance eqS1_default : DefaultRelation eqS1. +Instance eqS1_default : DefaultRelation eqS1 := {}. Axiom eqS1': S1 -> S1 -> Prop. Axiom SetoidS1' : Setoid_Theory S1 eqS1'. @@ -220,7 +220,7 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop. Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8. Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid. -Instance eqS1_test8_default : DefaultRelation eqS1_test8. +Instance eqS1_test8_default : DefaultRelation eqS1_test8 := {}. Axiom f_test8 : S2 -> S1_test8. Add Morphism f_test8 with signature (eqS2 ==> eqS1_test8) as f_compat_test8. Admitted. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 02a2348450..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --cur-version=8.9 || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? |