diff options
Diffstat (limited to 'test-suite')
24 files changed, 362 insertions, 49 deletions
diff --git a/test-suite/bugs/closed/bug_12414.v b/test-suite/bugs/closed/bug_12414.v new file mode 100644 index 0000000000..50b4b86eff --- /dev/null +++ b/test-suite/bugs/closed/bug_12414.v @@ -0,0 +1,13 @@ +Set Universe Polymorphism. +Set Printing Universes. +Inductive list {T} : Type := | cons (t : T) : list -> list. (* who needs nil anyway? *) +Arguments list : clear implicits. + +Fixpoint map {A B} (f: A -> B) (l : list A) : list B := + let '(cons t l) := l in cons (f t) (map f l). +About map@{_ _}. +(* Two universes, as expected. *) + +Definition map_Set@{} {A B : Set} := @map A B. + +Definition map_Prop@{} {A B : Prop} := @map A B. diff --git a/test-suite/bugs/closed/bug_12623.v b/test-suite/bugs/closed/bug_12623.v new file mode 100644 index 0000000000..9fdcb94e0c --- /dev/null +++ b/test-suite/bugs/closed/bug_12623.v @@ -0,0 +1,18 @@ +Set Universe Polymorphism. + +Axiom M : Type -> Prop. +Axiom raise : forall {T}, M T. + +Inductive goal : Type := +| AHyp : forall {A : Type}, goal. + +Definition gtactic@{u u0} := goal@{u} -> M@{u0} (False). + +Class Seq (C : Type) := + seq : C -> gtactic. +Arguments seq {C _} _. + +Instance seq_one : Seq@{Set _ _} (gtactic) := fun t2 => fun g => raise. + +Definition x1 : gtactic := @seq@{_ _ _} _ _ (fun g : goal => raise). +Definition x2 : gtactic := @seq@{_ _ _} _ seq_one (fun g : goal => raise). diff --git a/test-suite/bugs/closed/bug_12895.v b/test-suite/bugs/closed/bug_12895.v new file mode 100644 index 0000000000..53adc2981c --- /dev/null +++ b/test-suite/bugs/closed/bug_12895.v @@ -0,0 +1,20 @@ +Fixpoint bug_1 (e1 : nat) {struct e1} + : nat +with bug_2 {H_imp : nat} (e2 : nat) {struct e2} + : nat. +Proof. + - exact e1. + - exact e2. +Admitted. + +Fixpoint hbug_1 (a:bool) (e1 : nat) {struct e1} + : nat +with hbug_2 (a:nat) (e2 : nat) {struct e2} + : nat. +Proof. + - exact e1. + - exact e2. +Admitted. + +Check (hbug_1 : bool -> nat -> nat). +Check (hbug_2 : nat -> nat -> nat). diff --git a/test-suite/bugs/closed/bug_12970.v b/test-suite/bugs/closed/bug_12970.v new file mode 100644 index 0000000000..69ce7ec2c2 --- /dev/null +++ b/test-suite/bugs/closed/bug_12970.v @@ -0,0 +1,4 @@ +Arguments existT _ & _ _. + +Definition f := fun X (A : X -> Type) (P : forall x, A x -> Type) x y => + existT (fun f => forall x, P x (f x)) x y : sigT (fun f => forall x, P x (f x)). diff --git a/test-suite/bugs/closed/bug_13169.v b/test-suite/bugs/closed/bug_13169.v new file mode 100644 index 0000000000..a0b564c725 --- /dev/null +++ b/test-suite/bugs/closed/bug_13169.v @@ -0,0 +1,14 @@ +Goal False. +Proof. + set (H1:=I). + set (x:=true). + assert (H2: x = true) by reflexivity. + set (y:=false). + assert (H3: y = false) by reflexivity. + clearbody H1 x y. + eenough (H4: _ = false). + vm_compute in H4. + (* H4 now has "x:=y" in the evar context. *) + 2: exact H3. + match type of H4 with y = false => idtac end. +Abort. diff --git a/test-suite/bugs/closed/bug_13171.v b/test-suite/bugs/closed/bug_13171.v new file mode 100644 index 0000000000..0564722729 --- /dev/null +++ b/test-suite/bugs/closed/bug_13171.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Goal False. +Proof. + unshelve epose (_:nat). exact_no_check true. + Fail let c := open_constr:([| n | 0 |]) in + let c := eval cbv in c in + let c := type of c in + idtac c. +Abort. diff --git a/test-suite/bugs/closed/bug_5197.v b/test-suite/bugs/closed/bug_5197.v index 0c236e12ad..00b9e9bd9d 100644 --- a/test-suite/bugs/closed/bug_5197.v +++ b/test-suite/bugs/closed/bug_5197.v @@ -20,11 +20,11 @@ Definition Typeᶠ : TYPE := {| rel := fun _ A => (forall ω : Ω, A ω) -> Type; |}. Set Printing Universes. -Fail Definition Typeᵇ : El Typeᶠ := +Definition Typeᵇ : El Typeᶠ := mkPack _ _ (fun w => Type) (fun w A => (forall ω, A ω) -> Type). -Definition Typeᵇ : El Typeᶠ := - mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). +(* Definition Typeᵇ : El Typeᶠ := *) +(* mkPack _ (fun _ (A : Ω -> Type) => (forall ω : Ω, A ω) -> _) (fun w => Type) (fun w A => (forall ω, A ω) -> Type). *) (** Bidirectional typechecking helps here *) Require Import Program.Tactics. diff --git a/test-suite/ide/proof-diffs.fake b/test-suite/ide/proof-diffs.fake new file mode 100644 index 0000000000..594ebced23 --- /dev/null +++ b/test-suite/ide/proof-diffs.fake @@ -0,0 +1,10 @@ +ADD { Goal True /\ False /\ True = False. } +ADD { split. } +GOALS +ADD here { split. } +GOALS +PDIFF here +ADD there { auto. } +GOALS +PDIFF there +ADD { Admitted. } diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index abada44da7..bd22d45059 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -231,16 +231,13 @@ fun l : list nat => match l with : list nat -> list nat Arguments foo _%list_scope -Notation -"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope -(default interpretation) -"'exists' ! x .. y , p" := ex - (unique - (fun x => .. (ex (unique (fun y => p))) ..)) -: type_scope (default interpretation) -Notation -"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope -(default interpretation) +Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) + : type_scope (default interpretation) +Notation "'exists' ! x .. y , p" := + (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope + (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope + (default interpretation) 1 subgoal ============================ diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out index d45343fe60..7de1e7d559 100644 --- a/test-suite/output/Record.out +++ b/test-suite/output/Record.out @@ -30,3 +30,43 @@ 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 +{| a := 0; b := 0 |} + : T +fun '{| |} => 0 + : LongModuleName.test -> nat + = {| + a := + {| + LongModuleName.long_field_name0 := 0; + LongModuleName.long_field_name1 := 1; + LongModuleName.long_field_name2 := 2; + LongModuleName.long_field_name3 := 3 + |}; + b := + fun + '{| + LongModuleName.long_field_name0 := a; + LongModuleName.long_field_name1 := b; + LongModuleName.long_field_name2 := c; + LongModuleName.long_field_name3 := d + |} => (a, b, c, d) + |} + : T + = {| + a := + {| + long_field_name0 := 0; + long_field_name1 := 1; + long_field_name2 := 2; + long_field_name3 := 3 + |}; + b := + fun + '{| + long_field_name0 := a; + long_field_name1 := b; + long_field_name2 := c; + long_field_name3 := d + |} => (a, b, c, d) + |} + : T diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v index 71a8afa131..13ea37b11e 100644 --- a/test-suite/output/Record.v +++ b/test-suite/output/Record.v @@ -33,3 +33,34 @@ 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). + +Module FormattingIssue13142. + +Record T {A B} := {a:A;b:B}. + +Module LongModuleName. + Record test := { long_field_name0 : nat; + long_field_name1 : nat; + long_field_name2 : nat; + long_field_name3 : nat }. +End LongModuleName. + +Definition c := + {| LongModuleName.long_field_name0 := 0; + LongModuleName.long_field_name1 := 1; + LongModuleName.long_field_name2 := 2; + LongModuleName.long_field_name3 := 3 |}. + +Definition d := + fun '{| LongModuleName.long_field_name0 := a; + LongModuleName.long_field_name1 := b; + LongModuleName.long_field_name2 := c; + LongModuleName.long_field_name3 := d |} => (a,b,c,d). + +Check {|a:=0;b:=0|}. +Check fun '{| LongModuleName.long_field_name0:=_ |} => 0. +Eval compute in {|a:=c;b:=d|}. +Import LongModuleName. +Eval compute in {|a:=c;b:=d|}. + +End FormattingIssue13142. diff --git a/test-suite/output/bug_12908.out b/test-suite/output/bug_12908.out index fca6dde704..54c4f98422 100644 --- a/test-suite/output/bug_12908.out +++ b/test-suite/output/bug_12908.out @@ -1,2 +1,7 @@ forall m n : nat, m * n = (2 * m * n)%nat : Prop +File "stdin", line 11, characters 0-31: +Warning: Notation "_ * _" was already used in scope nat_scope. +[notation-overridden,parsing] +forall m n : nat, m * n = Nat.mul (Nat.mul 2 m) n + : Prop diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v index 558c9f9f6a..6f7be22fa0 100644 --- a/test-suite/output/bug_12908.v +++ b/test-suite/output/bug_12908.v @@ -1,6 +1,13 @@ Definition mult' m n := 2 * m * n. + Module A. (* Test hiding of a scoped notation by a lonely notation *) Infix "*" := mult'. Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End A. + +Module B. +(* Test that an overriden scoped notation is deactivated *) +Infix "*" := mult' : nat_scope. +Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. +End B. diff --git a/test-suite/output/bug_13112.out b/test-suite/output/bug_13112.out new file mode 100644 index 0000000000..a8a98d6b68 --- /dev/null +++ b/test-suite/output/bug_13112.out @@ -0,0 +1,4 @@ +0 + 0 + : nat +HI + : nat diff --git a/test-suite/output/bug_13112.v b/test-suite/output/bug_13112.v new file mode 100644 index 0000000000..9fee5e09d8 --- /dev/null +++ b/test-suite/output/bug_13112.v @@ -0,0 +1,5 @@ +Reserved Notation "'HI'". +Notation "'HI'" := (O + O) (only parsing). +Check HI. (* 0 + 0 : nat *) +Notation "'HI'" := (O + O) (only printing). +Check HI. (* 0 + 0 : nat *) diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out index ed4892b389..f035d0252a 100644 --- a/test-suite/output/bug_9180.out +++ b/test-suite/output/bug_9180.out @@ -1,4 +1,3 @@ -Notation -"n .+1" := S n : nat_scope (default interpretation) +Notation "n .+1" := (S n) : nat_scope (default interpretation) forall x : nat, x.+1 = x.+1 : Prop diff --git a/test-suite/output/bug_9682.out b/test-suite/output/bug_9682.out index e69de29bb2..45d9e4cad1 100644 --- a/test-suite/output/bug_9682.out +++ b/test-suite/output/bug_9682.out @@ -0,0 +1,9 @@ +mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x +return M (x = x) with +| 1 +end + : unit +# + : True +## + : True diff --git a/test-suite/output/bug_9682.v b/test-suite/output/bug_9682.v index 3630142126..fa30d323ef 100644 --- a/test-suite/output/bug_9682.v +++ b/test-suite/output/bug_9682.v @@ -16,3 +16,13 @@ Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" := (at level 200, ls at level 91, p at level 10, only printing, format "'[ ' mmatch '/' x ']' '/' '[ ' in '/' T ']' '/' '[ ' as '/' y ']' '/' '[ ' return M p ']' with '//' '[' ls ']' '//' end" ). +(* Check use of "mmatch" *) +Check (mmatch 1 + 2 + 3 + 4 + 5 + 6 in nat as x return M (x = x) with | 1 end). + +(* 2nd example *) +Notation "#" := I (at level 0, only parsing). +Notation "#" := I (at level 0, only printing). +Check #. +Notation "##" := I (at level 0, only printing). +Notation "##" := I (at level 0, only parsing). +Check ##. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 773533a8d3..17c1aaa55b 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -2,7 +2,79 @@ Nat.t = nat : Set Nat.t = nat : Set +2 subgoals + + ============================ + True + +subgoal 2 is: + True +2 subgoals, subgoal 1 (?Goal) + + ============================ + True + +subgoal 2 (?Goal0) is: + True 1 subgoal ============================ - False + True +1 subgoal (?Goal0) + + ============================ + True +1 subgoal (?Goal0) + + ============================ + True + +*** Unfocused goals: + +subgoal 2 (?Goal1) is: + True +subgoal 3 (?Goal) is: + True +1 subgoal + + ============================ + True + +*** Unfocused goals: + +subgoal 2 is: + True +subgoal 3 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +2 subgoals + +subgoal 1 is: + True +subgoal 2 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +2 subgoals + +subgoal 1 (?Goal0) is: + True +subgoal 2 (?Goal) is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +1 subgoal + +subgoal 1 is: + True +This subproof is complete, but there are some unfocused goals. +Focus next goal with bullet -. + +1 subgoal + +subgoal 1 (?Goal) is: + True diff --git a/test-suite/output/goal_output.v b/test-suite/output/goal_output.v index 327b80b0aa..b1ced94054 100644 --- a/test-suite/output/goal_output.v +++ b/test-suite/output/goal_output.v @@ -6,8 +6,32 @@ Print Nat.t. Timeout 1 Print Nat.t. -Lemma toto: False. Set Printing All. +Lemma toto: True/\True. +Proof. +split. Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. +assert True. +- idtac. +Show. +Set Printing Goal Names. +Show. +Set Printing Unfocused. +Show. +Unset Printing Goal Names. +Show. +Unset Printing Unfocused. + auto. +Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. +- auto. +Show. +Set Printing Goal Names. +Show. +Unset Printing Goal Names. Abort. - diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 473db2d312..93d9d6cf7b 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,3 +1,2 @@ -Notation -"b1 && b2" := if b1 then b2 else false (default interpretation) -"x && y" := andb x y : bool_scope +Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) +Notation "x && y" := (andb x y) : bool_scope diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 998f3f7dd1..73e98ea920 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -1,6 +1,8 @@ Require Import TestSuite.admit. (* compile en user 3m39.915s sur cachalot *) Require Import Nsatz. +Require List. +Import List.ListNotations. (* Example with a generic domain *) @@ -294,7 +296,7 @@ Lemma minh: forall A B C D O E H I:point, Proof. geo_begin. idtac "minh". Time nsatz with radicalmax :=1%N strategy:=1%Z - parameters:=(X O::X B::X C::nil) + parameters:=[X O; X B; X C] variables:= (@nil R). (*Finished transaction in 13. secs (10.102464u,0.s) *) @@ -314,15 +316,15 @@ Proof. geo_begin. idtac "Pappus". Time nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil) - variables:= (X B - :: X A1 - :: Y A1 - :: X B1 - :: Y B1 - :: X C - :: Y C1 - :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil). + parameters:=[X B; X A1; Y A1; X B1; Y B1; X C; Y C1] + variables:= [X B; + X A1; + Y A1; + X B1; + Y B1; + X C; + Y C1; + X C1; Y P; X P; Y Q; X Q; Y S; X S]. (*Finished transaction in 8. secs (7.795815u,0.000999999999999s) *) Qed. @@ -347,7 +349,7 @@ Proof. geo_begin. idtac "Simson". Time nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X B::Y B::X C::Y C::Y D::nil) + parameters:=[X B; Y B; X C; Y C; Y D] variables:= (@nil R). (* compute -[X Y]. *) (*Finished transaction in 8. secs (7.550852u,0.s) *) @@ -432,20 +434,20 @@ Proof. geo_begin. idtac "Desargues". Time -let lv := rev (X A - :: X B - :: Y B - :: X C - :: Y C - :: Y A1 :: X A1 - :: Y B1 - :: Y C1 - :: X T - :: Y T - :: X Q - :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in +let lv := rev [X A; + X B; + Y B; + X C; + Y C; + Y A1; X A1; + Y B1; + Y C1; + X T; + Y T; + X Q; + Y Q; X P; Y P; X C1; X B1] in nsatz with radicalmax :=1%N strategy:=0%Z - parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil) + parameters:=[X A; X B; Y B; X C; Y C; X A1; Y B1; Y C1] variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*) Qed. @@ -522,9 +524,9 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point, geo_begin. idtac "hauteurs". Time - let lv := constr:(Y A1 - :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C - :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in + let lv := constr:([Y A1; + X A1; Y B1; X B1; Y A; Y B; X B; X A; X H; Y C; + Y C1; Y H; X C1; X C]) in nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R) variables := lv. (*Finished transaction in 5. secs (4.360337u,0.008999s)*) diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index ce07512a1e..beb424dd40 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -93,3 +93,18 @@ Record R : Type := { (* This is used in a couple of development such as UniMatch *) Record S {A:Type} := { a : A; b : forall A:Type, A }. + +(* Bug #13165 on implicit arguments in defined fields *) +Record T := { + f {n:nat} (p:n=n) := nat; + g := f (eq_refl 0) +}. + +(* Slight improvement in when SProp relevance is detected *) +Inductive True : SProp := I. +Inductive eqI : True -> SProp := reflI : eqI I. + +Record U (c:True) := { + u := c; + v := reflI : eqI u; + }. diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 9ab8ace39e..0796b507a1 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -457,5 +457,10 @@ Module ObligationRegression. (** Test for a regression encountered when fixing obligations for stronger restriction of universe context. *) Require Import CMorphisms. - Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _ _}. + Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _ _ _}. End ObligationRegression. + +Axiom poly@{i} : forall(A : Type@{i}) (a : A), unit. + +Definition nonpoly := @poly True Logic.I. +Definition check := nonpoly@{}. |