diff options
Diffstat (limited to 'test-suite')
33 files changed, 527 insertions, 71 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_12917.v b/test-suite/bugs/closed/bug_12917.v new file mode 100644 index 0000000000..cd6b0766c6 --- /dev/null +++ b/test-suite/bugs/closed/bug_12917.v @@ -0,0 +1 @@ +Fail Derive Inversion bla with (le _ _). diff --git a/test-suite/bugs/closed/bug_12947.v b/test-suite/bugs/closed/bug_12947.v new file mode 100644 index 0000000000..baf0579465 --- /dev/null +++ b/test-suite/bugs/closed/bug_12947.v @@ -0,0 +1,9 @@ +Require Import BinPos Int63 PArray. + +Definition foo (n : positive) := + let a := make 2 0 in + let b := Pos.iter (fun b => set b 1 1) a 100000 in + let v := get b 0 in + Pos.iter (fun v => v + get a 0) v n. + +Timeout 5 Time Eval vm_compute in foo 1000000. 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_13086.v b/test-suite/bugs/closed/bug_13086.v new file mode 100644 index 0000000000..75f842b1cf --- /dev/null +++ b/test-suite/bugs/closed/bug_13086.v @@ -0,0 +1,11 @@ +Unset Universe Checking. + +Definition bad1@{|Set < Set} := Prop. + +Set Universe Polymorphism. +Axiom ax : Type. +Inductive I@{u} : Prop := foo : ax@{u} -> I. + +Definition bad2@{v} (x:I@{v}) : I@{Set} := x. + +Definition vsdvds (f : (Prop -> Prop) -> Prop) (x : Set -> Prop) := f x. diff --git a/test-suite/bugs/closed/bug_13117.v b/test-suite/bugs/closed/bug_13117.v new file mode 100644 index 0000000000..5db3f9fadc --- /dev/null +++ b/test-suite/bugs/closed/bug_13117.v @@ -0,0 +1,23 @@ + +Class A := {}. + +Class B (x:A) := {}. +Class B' (a:=A) (x:a) := {}. + +Fail Definition foo a `{B a} := 0. +Definition foo a `{B' a} := 0. + +Record C (x:A) := {}. +Existing Class C. + +Fail Definition bar a `{C a} := 0. + + +Definition X := Type. + +Class Y (x:X) := {}. + +Definition before `{Y Set} := 0. + +Existing Class X. +Fail Definition after `{Y Set} := 0. diff --git a/test-suite/bugs/closed/bug_13129.v b/test-suite/bugs/closed/bug_13129.v new file mode 100644 index 0000000000..632605ecc7 --- /dev/null +++ b/test-suite/bugs/closed/bug_13129.v @@ -0,0 +1,58 @@ +From Coq Require Export Morphisms Setoid . + +Class Equiv A := equiv: relation A. + +Infix "≡" := equiv (at level 70, no associativity). +Infix "≡@{ A }" := (@equiv A _) + (at level 70, only parsing, no associativity). + +Notation "(≡)" := equiv (only parsing). + +(** Unbundled version *) +Class Dist A := dist : nat -> relation A. + +Notation "x ≡{ n }≡ y" := (dist n x y) + (at level 70, n at next level, format "x ≡{ n }≡ y"). +Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y) + (at level 70, n at next level, only parsing). + +Notation NonExpansive f := (forall n, Proper (dist n ==> dist n ==> dist n) f). + +Record OfeMixin A `{Equiv A, Dist A} := { + mixin_equiv_dist (x y : A) : x ≡ y <-> forall n, x ≡{n}≡ y; +}. + +(** Bundled version *) +Structure ofeT := OfeT { + ofe_car :> Type; + ofe_equiv : Equiv ofe_car; + ofe_dist : Dist ofe_car; + ofe_mixin : OfeMixin ofe_car +}. +Hint Extern 0 (Equiv _) => eapply (@ofe_equiv _) : typeclass_instances. +Hint Extern 0 (Dist _) => eapply (@ofe_dist _) : typeclass_instances. + +(** Lifting properties from the mixin *) +Section ofe_mixin. + Context {A : ofeT}. + Implicit Types x y : A. + Lemma equiv_dist x y : x ≡ y <-> forall n, x ≡{n}≡ y. + Proof. apply (mixin_equiv_dist _ (ofe_mixin A)). Qed. +End ofe_mixin. + +Axiom _0 : Prop. (* dummy which somehow bothers mangle names *) +Set Mangle Names. + +(** General properties *) +Section ofe. + Context {A : ofeT}. + + Lemma ne_proper_2 {B C : ofeT} (f : A -> B -> C) `{Hf:!NonExpansive f} : + Proper ((≡) ==> (≡) ==> (≡)) f. + Proof. + unfold Proper, respectful. + setoid_rewrite equiv_dist. + intros. + apply Hf;auto. + Qed. +End ofe. 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/micromega/int63.v b/test-suite/micromega/int63.v new file mode 100644 index 0000000000..20dfa2631e --- /dev/null +++ b/test-suite/micromega/int63.v @@ -0,0 +1,24 @@ +Require Import ZArith ZifyInt63 Lia. +Require Import Int63. + +Open Scope int63_scope. + +Goal forall (x:int), 0 <= x = true. +Proof. lia. Qed. + +Goal max_int = 9223372036854775807. +Proof. lia. Qed. + +Goal digits = 63. +Proof. lia. Qed. + +Goal wB = (2^63)%Z. +Proof. lia. Qed. + +Goal forall x y, x + y <= max_int = true. +Proof. lia. Qed. + +Goal forall x, x <> 0 -> x / x = 1. +Proof. + nia. +Qed. diff --git a/test-suite/output/DependentInductionErrors.out b/test-suite/output/DependentInductionErrors.out new file mode 100644 index 0000000000..4a83375f6f --- /dev/null +++ b/test-suite/output/DependentInductionErrors.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +Tactic failure: To use dependent destruction, first [Require Import Coq.Program.Equality.]. +The command has indeed failed with message: +Tactic failure: To use dependent induction, first [Require Import Coq.Program.Equality.]. diff --git a/test-suite/output/DependentInductionErrors.v b/test-suite/output/DependentInductionErrors.v new file mode 100644 index 0000000000..2fce00f9fd --- /dev/null +++ b/test-suite/output/DependentInductionErrors.v @@ -0,0 +1,17 @@ +Theorem foo (b:bool) : b = true \/ b = false. +Proof. + Fail dependent destruction b. + Fail dependent induction b. +Abort. + +From Coq Require Import Program.Equality. + +Theorem foo_with_destruction (b:bool) : b = true \/ b = false. +Proof. + dependent destruction b; auto. +Qed. + +Theorem foo_with_induction (b:bool) : b = true \/ b = false. +Proof. + dependent induction b; auto. +Qed. 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 new file mode 100644 index 0000000000..45d9e4cad1 --- /dev/null +++ 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 new file mode 100644 index 0000000000..fa30d323ef --- /dev/null +++ b/test-suite/output/bug_9682.v @@ -0,0 +1,28 @@ +Declare Scope blafu. +Delimit Scope blafu with B. +Axiom DoesNotMatch : Type. +Axiom consumer : forall {A} (B : A -> Type) (E:Type) (x : A) (ls : list nat), unit. + +Notation "| p1 | .. | pn" := (@cons _ p1 .. (@cons _ pn nil) ..) (at level 91) : blafu. +Notation "'mmatch_do_not_write' x 'in' T 'as' y 'return' 'M' p 'with_do_not_write' ls" := + (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B) + (at level 200, ls at level 91, only parsing). +Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" := + (mmatch_do_not_write x in T as y return M p with_do_not_write ls) + (at level 200, ls at level 91, p at level 10, only parsing). +(* This should not gives a warning *) +Notation "'mmatch' x 'in' T 'as' y 'return' 'M' p 'with' ls 'end'" := + (@consumer _ (fun y : T => p%type) DoesNotMatch x ls%B) + (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/primitive/arrays/reroot.v b/test-suite/primitive/arrays/reroot.v deleted file mode 100644 index 172a118cc7..0000000000 --- a/test-suite/primitive/arrays/reroot.v +++ /dev/null @@ -1,22 +0,0 @@ -From Coq Require Import Int63 PArray. - -Open Scope array_scope. - -Definition t : array nat := [| 1; 5; 2 | 4 |]. -Definition t' : array nat := PArray.reroot t. - -Definition foo1 := (eq_refl : t'.[1] = 5). -Definition foo2 := (eq_refl 5 <: t'.[1] = 5). -Definition foo3 := (eq_refl 5 <<: t'.[1] = 5). -Definition x1 := Eval compute in t'.[1]. -Definition foo4 := (eq_refl : x1 = 5). -Definition x2 := Eval cbn in t'.[1]. -Definition foo5 := (eq_refl : x2 = 5). - -Definition foo6 := (eq_refl : t.[1] = 5). -Definition foo7 := (eq_refl 5 <: t.[1] = 5). -Definition foo8 := (eq_refl 5 <<: t.[1] = 5). -Definition x3 := Eval compute in t.[1]. -Definition foo9 := (eq_refl : x3 = 5). -Definition x4 := Eval cbn in t.[1]. -Definition foo10 := (eq_refl : x4 = 5). 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@{}. |