diff options
Diffstat (limited to 'test-suite')
25 files changed, 541 insertions, 60 deletions
diff --git a/test-suite/bugs/closed/bug_11515.v b/test-suite/bugs/closed/bug_11515.v new file mode 100644 index 0000000000..fe4ba87447 --- /dev/null +++ b/test-suite/bugs/closed/bug_11515.v @@ -0,0 +1,7 @@ +Require Import Ltac2.Ltac2. + +Lemma foo : + True. +Proof. + Fail rewrite _. +Abort. diff --git a/test-suite/bugs/closed/bug_11553.v b/test-suite/bugs/closed/bug_11553.v new file mode 100644 index 0000000000..a4a4353cd6 --- /dev/null +++ b/test-suite/bugs/closed/bug_11553.v @@ -0,0 +1,34 @@ +Definition var := nat. +Module Import A. +Class Rename (term : Type) := rename : (var -> var) -> term -> term. +End A. + +Inductive tm : Type := + (* | tv : vl_ -> tm *) + with vl_ : Type := + | var_vl : var -> vl_. + +Definition vl := vl_. + +Fixpoint tm_rename (sb : var -> var) (t : tm) : tm := + let b := vl_rename : Rename vl in + match t with + end +with +vl_rename (sb : var -> var) v : vl := + let a := tm_rename : Rename tm in + let b := vl_rename : Rename vl in + match v with + | var_vl x => var_vl (sb x) + end. + +Instance rename_vl : Rename vl := vl_rename. + +Lemma foo ξ x: rename_vl ξ (var_vl x) = var_vl x. +(* Succeeds *) +cbn. Abort. + +Lemma foo ξ x: rename ξ (var_vl x) = var_vl x. +(* Fails *) +cbn. +Abort. diff --git a/test-suite/bugs/closed/bug_5617.v b/test-suite/bugs/closed/bug_5617.v new file mode 100644 index 0000000000..c18e79295c --- /dev/null +++ b/test-suite/bugs/closed/bug_5617.v @@ -0,0 +1,8 @@ +Set Primitive Projections. +Record T X := { F : X }. + +Fixpoint f (n : nat) : nat := +match n with +| 0 => 0 +| S m => F _ {| F := f |} m +end. diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v deleted file mode 100644 index fbd9c8bcba..0000000000 --- a/test-suite/failure/Template.v +++ /dev/null @@ -1,28 +0,0 @@ - -Module TestUnsetTemplateCheck. - Unset Template Check. - - Section Foo. - - Context (A : Type). - - Definition cstr := nat : ltac:(let ty := type of A in exact ty). - - Inductive myind := - | cons : A -> myind. - End Foo. - - (* Can only succeed if no template check is performed *) - Check myind True : Prop. - - About myind. - - (* test discharge puts things in the right order (by using the - checker on the result) *) - Section S. - - Variables (A:Type) (a:A). - Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B. - End S. - -End TestUnsetTemplateCheck. diff --git a/test-suite/ltac2/array_lib.v b/test-suite/ltac2/array_lib.v new file mode 100644 index 0000000000..31227eaddb --- /dev/null +++ b/test-suite/ltac2/array_lib.v @@ -0,0 +1,181 @@ +Require Import Ltac2.Ltac2. +Import Ltac2.Message. +Import Ltac2.Array. +Require Ltac2.List. +Require Ltac2.Int. + +(* Array/List comparison functions which throw an exception on unequal *) + +Ltac2 Type exn ::= [ Regression_Test_Failure ]. + +Ltac2 check_eq_int a l := + List.iter2 + (fun a b => match Int.equal a b with true => () | false => Control.throw Regression_Test_Failure end) + (to_list a) l. + +Ltac2 check_eq_bool a l := + List.iter2 + (fun a b => match Bool.eq a b with true => () | false => Control.throw Regression_Test_Failure end) + (to_list a) l. + +Ltac2 check_eq_int_matrix m ll := + List.iter2 (fun a b => check_eq_int a b) (to_list m) ll. + +Ltac2 check_eq_bool_matrix m ll := + List.iter2 (fun a b => check_eq_bool a b) (to_list m) ll. + +(* The below printing functions are mostly for debugging below test cases *) + +Ltac2 print2 m1 m2 := print (Message.concat m1 m2). +Ltac2 print3 m1 m2 m3 := print2 m1 (Message.concat m2 m3). + +Ltac2 print_int_array a := + iteri (fun i x => print3 (of_int i) (of_string "=") (of_int x)) a. + +Ltac2 of_bool b := match b with true=>of_string "true" | false=>of_string "false" end. + +Ltac2 print_bool_array a := + iteri (fun i x => print3 (of_int i) (of_string "=") (of_bool x)) a. + +Ltac2 print_int_list a := + List.iteri (fun i x => print3 (of_int i) (of_string "=") (of_int x)) a. + +Goal True. + (* Test failure *) + Fail check_eq_int ((init 3 (fun i => (Int.add i 10)))) [10;11;13]. + + (* test empty with int *) + check_eq_int (empty ()) []. + check_eq_int (append (empty ()) (init 3 (fun i => (Int.add i 10)))) [10;11;12]. + check_eq_int (append (init 3 (fun i => (Int.add i 10))) (empty ())) [10;11;12]. + + (* test empty with bool *) + check_eq_bool (empty ()) []. + check_eq_bool (append (empty ()) (init 3 (fun i => (Int.ge i 2)))) [false;false;true]. + check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) (empty ())) [false;false;true]. + + (* test init with int *) + check_eq_int (init 0 (fun i => (Int.add i 10))) []. + check_eq_int (init 4 (fun i => (Int.add i 10))) [10;11;12;13]. + + (* test init with bool *) + check_eq_bool (init 0 (fun i => (Int.ge i 2))) []. + check_eq_bool (init 4 (fun i => (Int.ge i 2))) [false;false;true;true]. + + (* test make_matrix, set, get *) + let a := make_matrix 4 3 1 in + Array.set (Array.get a 1) 2 0; + check_eq_int_matrix a [[1;1;1];[1;1;0];[1;1;1];[1;1;1]]. + + let a := make_matrix 3 4 false in + Array.set (Array.get a 2) 1 true; + check_eq_bool_matrix a [[false;false;false;false];[false;false;false;false];[false;true;false;false]]. + + (* test copy *) + let a := init 4 (fun i => (Int.add i 10)) in + let b := copy a in + check_eq_int b [10;11;12;13]. + + (* test append *) + let a := init 3 (fun i => (Int.add i 10)) in + let b := init 4 (fun i => (Int.add i 20)) in + check_eq_int (append a b) [10;11;12;20;21;22;23]. + + (* test concat *) + let a := init 3 (fun i => (Int.add i 10)) in + let b := init 4 (fun i => (Int.add i 20)) in + let c := init 5 (fun i => (Int.add i 30)) in + check_eq_int (concat (a::b::c::[])) [10;11;12;20;21;22;23;30;31;32;33;34]. + + (* test sub *) + let a := init 10 (fun i => (Int.add i 10)) in + let b := (sub a 3 0) in + let c := (append b (init 3 (fun i => (Int.add i 10)))) in + check_eq_int b []; + check_eq_int c [10;11;12]. + + let a := init 10 (fun i => (Int.add i 10)) in + let b := (sub a 3 4) in + check_eq_int b [13;14;15;16]. + + (* test fill *) + let a := init 10 (fun i => (Int.add i 10)) in + fill a 3 4 0; + check_eq_int a [10;11;12;0;0;0;0;17;18;19]. + + (* test blit *) + let a := init 10 (fun i => (Int.add i 10)) in + let b := init 10 (fun i => (Int.add i 20)) in + blit a 5 b 3 4; + check_eq_int b [20;21;22;15;16;17;18;27;28;29]. + + (* test iter *) + let a := init 4 (fun i => (Int.add i 3)) in + let b := init 10 (fun i => 10) in + iter (fun x => Array.set b x x) a; + check_eq_int b [10;10;10;3;4;5;6;10;10;10]. + + (* test iter2 *) + let a := init 4 (fun i => (Int.add i 2)) in + let b := init 4 (fun i => (Int.add i 4)) in + let c := init 8 (fun i => 10) in + iter2 (fun x y => Array.set c x y) a b; + check_eq_int c [10;10;4;5;6;7;10;10]. + + (* test map *) + let a := init 4 (fun i => (Int.add i 10)) in + check_eq_bool (map (fun i => (Int.ge i 12)) a) [false;false;true;true]. + + (* test map2 *) + let a := init 4 (fun i => (Int.add 10 i)) in + let b := init 4 (fun i => (Int.sub 13 i)) in + check_eq_bool (map2 (fun x y => (Int.ge x y)) a b) [false;false;true;true]. + + (* test iteri *) + let a := init 4 (fun i => (Int.add i 10)) in + let m := make_matrix 4 2 100 in + iteri (fun i x => Array.set (Array.get m i) 0 i; Array.set (Array.get m i) 1 x) a; + check_eq_int_matrix m [[0;10];[1;11];[2;12];[3;13]]. + + (* test mapi *) + let a := init 4 (fun i => (Int.sub 3 i)) in + check_eq_bool (mapi (fun i x => (Int.ge i x)) a) [false;false;true;true]. + + (* to_list is already tested in check_eq_... *) + + (* test of_list *) + check_eq_int (of_list ([0;1;2;3])) [0;1;2;3]. + + (* test fold_left *) + let a := init 4 (fun i => (Int.add 10 i)) in + check_eq_int (of_list (fold_left (fun a b => b::a) [] a)) [13;12;11;10]. + + (* test fold_right *) + let a := init 4 (fun i => (Int.add 10 i)) in + check_eq_int (of_list (fold_right (fun a b => b::a) [] a)) [10;11;12;13]. + + (* test exist *) + let a := init 4 (fun i => (Int.add 10 i)) in + let l := [ + exist (fun x => Int.equal x 10) a; + exist (fun x => Int.equal x 13) a; + exist (fun x => Int.equal x 14) a] in + check_eq_bool (of_list l) [true;true;false]. + + (* test for_all *) + let a := init 4 (fun i => (Int.add 10 i)) in + let l := [ + for_all (fun x => Int.lt x 14) a; + for_all (fun x => Int.lt x 13) a] in + check_eq_bool (of_list l) [true;false]. + + (* test mem *) + let a := init 4 (fun i => (Int.add 10 i)) in + let l := [ + mem Int.equal 10 a; + mem Int.equal 13 a; + mem Int.equal 14 a] in + check_eq_bool (of_list l) [true;true;false]. + +exact I. +Qed. diff --git a/test-suite/micromega/bug_11436.v b/test-suite/micromega/bug_11436.v new file mode 100644 index 0000000000..fc6ccbb233 --- /dev/null +++ b/test-suite/micromega/bug_11436.v @@ -0,0 +1,19 @@ +Require Import ZArith Lia. +Local Open Scope Z_scope. + +Unset Lia Cache. + +Goal forall a q q0 q1 r r0 r1: Z, + 0 <= a < 2 ^ 64 -> + r1 = 4 * q + r -> + 0 <= r < 4 -> + a = 4 * q0 + r0 -> + 0 <= r0 < 4 -> + a + 4 = 2 ^ 64 * q1 + r1 -> + 0 <= r1 < 2 ^ 64 -> + r = r0. +Proof. + intros. + (* subst. *) + Time lia. +Qed. diff --git a/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v new file mode 100644 index 0000000000..a53c160e45 --- /dev/null +++ b/test-suite/micromega/evars_loops_in_8_10_fixed_8_11.v @@ -0,0 +1,4 @@ +Require Import Lia. +Goal forall n (B: n >= 0), exists Goal1 Goal2 Goal3, + (0 * (Goal1 * Goal2 + Goal1) <> Goal3 * 0 * (Goal1 * S Goal2)). +Proof. eexists _, _, _. Fail lia. Abort. diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 9efb81a901..36b4243ef8 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -11,15 +11,14 @@ Open Scope Z_scope. Lemma Zabs_square : forall x, (Z.abs x)^2 = x^2. Proof. - intros ; case (Zabs_dec x) ; intros ; nia. + intros ; nia. Qed. -Hint Resolve Z.abs_nonneg Zabs_square. Lemma integer_statement : ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0. Proof. intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p). assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2 - /\ Z.abs p^2 = p^2) by auto. + /\ Z.abs p^2 = p^2) by auto using Z.abs_nonneg, Zabs_square. assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; nia). generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear. @@ -45,10 +44,7 @@ Proof. intros. destruct x. simpl. - unfold Z.pow_pos. - simpl. - rewrite Pos.mul_1_r. - reflexivity. + lia. Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 5093e785de..26ebd8efc3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -86,8 +86,8 @@ Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: Some argument names are duplicated: F The command has indeed failed with message: -Argument number 2 (anonymous in original definition) cannot be declared -implicit. +Argument number 3 is a trailing implicit, so it can't be declared non +maximal. Please use { } instead of [ ]. The command has indeed failed with message: Extra arguments: y. The command has indeed failed with message: diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index 9713a9dbbe..6ac09cf771 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -49,7 +49,6 @@ Check @myplus. Fail Arguments eq_refl {F g}, [H] k. Fail Arguments eq_refl {F}, [F] : rename. Fail Arguments eq_refl {F F}, [F] F : rename. -Fail Arguments eq {F} x [z] : rename. +Fail Arguments eq {A} x [z] : rename. Fail Arguments eq {F} x z y. Fail Arguments eq {R} s t. - diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 6879cbc3c2..60bc9cbf55 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -1,8 +1,8 @@ -fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : -list B := match l with - | nil => nil - | a :: l0 => f a :: F A B f l0 - end +fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B := + match l with + | nil => nil + | a :: l0 => f a :: F A B f l0 + end : forall A B : Set, (A -> B) -> list A -> list B let fix f (m : nat) : nat := match m with | 0 => 0 diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index c142d28ebe..0a989646cf 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -61,3 +61,18 @@ H : a = 0 -> forall a : nat, a = 0 ============================ a = 0 +File "stdin", line 101, characters 47-48: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 105, characters 36-37: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 106, characters 34-35: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 112, characters 22-23: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] +File "stdin", line 112, characters 30-31: +Warning: Ignoring implicit binder declaration in unexpected position. +[unexpected-implicit-declaration,syntax] diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 7f3b332d7d..610fa48c0c 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -90,3 +90,25 @@ apply H with (a:=a). (* test compliance with printing *) Abort. End A. + +Module B. + +(* Check valid/invalid implicit arguments *) +Definition f1 {x} (y:forall {x}, x=0) := x+0. +Definition f2 := (((fun x => 0):forall {x:nat}, nat), 0). +Definition f3 := fun {x} (y:forall {x}, x=0) => x+0. + +Definition g1 {x} := match x with true => fun {x:bool} => x | false => fun x:bool => x end. +(* TODO: do not ignore the implicit here *) +Definition g2 '(x,y) {z} := x+y+z. + +Definition h1 := fun x:nat => (fun {x} => x) 0. +Definition h2 := let g := forall {y}, y=0 in g. + +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity, + format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. + +Definition l1 := ∀ {x:nat} {y:nat}, x=0. + +End B. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 94b86fc222..b870fa6f6f 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -137,3 +137,71 @@ end = p : forall x : nat, x = x -> Prop bar 0 : nat +let k := rew [P] p in v in k + : P y +let k := rew [P] p in v in k + : P y +let k := rew <- [P] p in v' in k + : P x +let k := rew [P] p in v in k + : P y +let k := rew [P] p in v in k + : P y +let k := rew <- [P] p in v' in k + : P x +let k := rew [fun y : A => P y] p in v in k + : P y +let k := rew [fun y : A => P y] p in v in k + : P y +let k := rew <- [fun y : A => P y] p in v' in k + : P x +let k := rew [fun y : A => P y] p in v in k + : P y +let k := rew [fun y : A => P y] p in v in k + : P y +let k := rew <- [fun y : A => P y] p in v' in k + : P x +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent <- [P'] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent <- [P'] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent <- [P'] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [fun y p => id (P y p)] p in v in k + : P y p +let k := rew dependent [fun y p => id (P y p)] p in v in k + : P y p +let k := rew dependent <- [fun y0 p => id (P' y0 p)] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent [P] p in v in k + : P y p +let k := rew dependent <- [P'] p in v' in k + : P' x (eq_sym p) +let k := rew dependent [fun y p0 => id (P y p0)] p in v in k + : P y p +let k := rew dependent [fun y p0 => id (P y p0)] p in v in k + : P y p +let k := rew dependent <- [fun y0 p0 => id (P' y0 p0)] p in v' in k + : P' x (eq_sym p) +rew dependent [P] p in v + : P y p +rew dependent <- [P'] p in v' + : P' x (eq_sym p) +rew dependent [fun a x => id (P a x)] p in v + : id (P y p) +rew dependent <- [fun a p' => id (P' a p')] p in v' + : id (P' x (eq_sym p)) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index adab324cf0..7d2f1e9ba8 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -251,11 +251,11 @@ Notation NONE := None. Check (fun x => match x with SOME x => x | NONE => 0 end). Notation NONE2 := (@None _). -Notation SOME2 := (@Some _). +Notation SOME2 := (@Some _). Check (fun x => match x with SOME2 x => x | NONE2 => 0 end). Notation NONE3 := @None. -Notation SOME3 := @Some. +Notation SOME3 := @Some. Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end). Notation "a :'" := (cons a) (at level 12). @@ -300,3 +300,61 @@ Definition bar (a b : nat) := plus a b. Notation "" := A (format "", only printing). Check (bar A 0). End M. + +(* Check eq notations *) +Module EqNotationsCheck. + Import EqNotations. + Section nd. + Context (A : Type) (x : A) (P : A -> Type) + (y : A) (p : x = y) (v : P x) (v' : P y). + + Check let k : P y := rew p in v in k. + Check let k : P y := rew -> p in v in k. + Check let k : P x := rew <- p in v' in k. + Check let k : P y := rew [P] p in v in k. + Check let k : P y := rew -> [P] p in v in k. + Check let k : P x := rew <- [P] p in v' in k. + Check let k : P y := rew [fun y => P y] p in v in k. + Check let k : P y := rew -> [fun y => P y] p in v in k. + Check let k : P x := rew <- [fun y => P y] p in v' in k. + Check let k : P y := rew [fun (y : A) => P y] p in v in k. + Check let k : P y := rew -> [fun (y : A) => P y] p in v in k. + Check let k : P x := rew <- [fun (y : A) => P y] p in v' in k. + End nd. + Section dep. + Context (A : Type) (x : A) (P : forall y, x = y -> Type) + (y : A) (p : x = y) (P' : forall x, y = x -> Type) + (v : P x eq_refl) (v' : P' y eq_refl). + + Check let k : P y p := rew dependent p in v in k. + Check let k : P y p := rew dependent -> p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- p in v' in k. + Check let k : P y p := rew dependent [P] p in v in k. + Check let k : P y p := rew dependent -> [P] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [P'] p in v' in k. + Check let k : P y p := rew dependent [fun y p => P y p] p in v in k. + Check let k : P y p := rew dependent -> [fun y p => P y p] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => P' y p] p in v' in k. + Check let k : P y p := rew dependent [fun y p => id (P y p)] p in v in k. + Check let k : P y p := rew dependent -> [fun y p => id (P y p)] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [fun y p => id (P' y p)] p in v' in k. + Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => P y p)] p in v in k. + Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => P y p)] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => P' x p)] p in v' in k. + Check let k : P y p := rew dependent [(fun (y : A) (p : x = y) => id (P y p))] p in v in k. + Check let k : P y p := rew dependent -> [(fun (y : A) (p : x = y) => id (P y p))] p in v in k. + Check let k : P' x (eq_sym p) := rew dependent <- [(fun (x : A) (p : y = x) => id (P' x p))] p in v' in k. + Check match p as x in _ = a return P a x with + | eq_refl => v + end. + Check match eq_sym p as p' in _ = a return P' a p' with + | eq_refl => v' + end. + Check match p as x in _ = a return id (P a x) with + | eq_refl => v + end. + Check match eq_sym p as p' in _ = a return id (P' a p') with + | eq_refl => v' + end. + End dep. +End EqNotationsCheck. diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index aeebc0f98b..839df99ea7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -219,8 +219,8 @@ Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. Module G. Generalizable Variables A R. Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x. -Check exists_true `{Reflexive A R}, forall x, R x x. -Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z. +Check exists_true `(Reflexive A R), forall x, R x x. +Check exists_true x `(Reflexive A R) y, x+y=0 -> forall z, R z z. End G. (* Allows recursive patterns for binders to be associative on the left *) diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 799d310fa7..f65696e464 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -4,11 +4,11 @@ Entry constr:myconstr is [ "6" RIGHTA [ ] | "5" RIGHTA - [ SELF; "+"; NEXT ] + [ SELF; "+"; NEXT ] | "4" RIGHTA - [ SELF; "*"; NEXT ] + [ SELF; "*"; NEXT ] | "3" RIGHTA - [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [ "<"; constr:operconstr LEVEL "10"; ">" ] ] [< b > + < b > * < 2 >] : nat @@ -63,3 +63,11 @@ fun '{| |} => true : R -> bool b = a : Prop +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". +The command has indeed failed with message: +The format is not the same on the right- and left-hand sides of the special token "..". diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 26c7840a16..4de6ce19b4 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -158,3 +158,29 @@ Check b = a. End Test. End L. + +Module M. + +(* Accept boxes around the end variables of a recursive notation (if equal boxes) *) + +Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[v' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +Fail Notation " {@ T1 ; T2 ; .. ; Tn } " := + (and T1 (and T2 .. (and Tn True)..)) + (format "'[v' {@ '[' T1 ']' ; '//' '[' T2 ']' ; '//' .. ; '//' '[' Tn ']' } ']'"). + +End M. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 3f4d5ef58c..190c34262f 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -3,6 +3,10 @@ foo : nat Axioms: foo : nat Axioms: +bli : Type +Axioms: +bli : Type +Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index 3d4dfe603d..4c980fddba 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -30,6 +30,21 @@ Module P := N M. Print Assumptions M.bar. (* Should answer: foo *) Print Assumptions P.bar. (* Should answer: foo *) +(* Print Assumptions used empty instances on polymorphic inductives *) +Module Poly. + + Set Universe Polymorphism. + Axiom bli : Type. + + Definition bla := bli -> bli. + + Inductive blo : bli -> Type := . + + Print Assumptions bla. + Print Assumptions blo. + +End Poly. + (* The original test-case of the bug-report *) diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v deleted file mode 100644 index dd259988ac..0000000000 --- a/test-suite/success/CompatOldOldFlag.v +++ /dev/null @@ -1,6 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) -(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. -Import Coq.Compat.Coq810. -Import Coq.Compat.Coq89. diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v index de34e007d2..df729588f4 100644 --- a/test-suite/success/Generalization.v +++ b/test-suite/success/Generalization.v @@ -11,4 +11,10 @@ Admitted. Print a_eq_b. +Require Import Morphisms. +Class Equiv A := equiv : A -> A -> Prop. +Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv). + +Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True. +Admitted. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index b16e4a1186..e68040e4d4 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -1,3 +1,15 @@ + +Axiom foo : forall (x y z t : nat), nat. + +Arguments foo {_} _ [z] t. +Check (foo 1). +Arguments foo {_} _ {z} {t}. +Fail Arguments foo {_} _ [z] {t}. +Check (foo 1). + +Definition foo1 [m] n := n + m. +Check (foo1 1). + Inductive vector {A : Type} : nat -> Type := | vnil : vector 0 | vcons : A -> forall {n'}, vector n' -> vector (S n'). @@ -33,3 +45,11 @@ Abort. 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. + +Inductive A' {P:forall m [n], n=m -> Prop} := C' : P 0 eq_refl -> A'. +Inductive A'' [P:forall m {n}, n=m -> Prop] (b : bool):= C'' : P 0 eq_refl -> A'' b. +Inductive A''' (P:forall m [n], n=m -> Prop) (b : bool):= C''' : P 0 eq_refl -> A''' P b. + +Definition F (id: forall [A] [x : A], A) := id. +Definition G := let id := (fun [A] (x : A) => x) in id. +Fail Definition G' := let id := (fun {A} (x : A) => x) in id. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index ecaaedca53..59650d6822 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -114,9 +114,13 @@ Check h 0. Inductive I {A} (a:A) : forall {n:nat}, Prop := | C : I a (n:=0). +Inductive I' [A] (a:A) : forall [n:nat], n =0 -> Prop := + | C' : I' a eq_refl. + Inductive I2 (x:=0) : Prop := - | C2 {p:nat} : p = 0 -> I2. -Check C2 eq_refl. + | C2 {p:nat} : p = 0 -> I2 + | C2' [p:nat] : p = 0 -> I2. +Check C2' eq_refl. Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := | C3 : I3 a (n:=0). @@ -147,6 +151,7 @@ Set Warnings "syntax". (* Miscellaneous tests *) Check let f := fun {x:nat} y => y=true in f false. +Check let f := fun [x:nat] y => y=true in f false. (* Isn't the name "arg_1" a bit fragile, here? *) @@ -157,3 +162,23 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0). Set Warnings "+syntax". Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)). Set Warnings "syntax". + + +Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0. +Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0. +Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0. +Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted. +Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0. + +Module TestUnnamedImplicit. + +Axiom foo : forall A, A -> A. + +Arguments foo {A} {_}. +Check foo (arg_2:=true) : bool. +Check foo : bool. + +Arguments foo {A} {x}. +Check foo (x:=true) : bool. + +End TestUnnamedImplicit. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 61273c4f37..7ff5571ffb 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 --master || exit $? +dev/tools/update-compat.py --assert-unchanged --release || exit $? |