diff options
Diffstat (limited to 'test-suite')
27 files changed, 622 insertions, 166 deletions
diff --git a/test-suite/.csdp.cache.test-suite b/test-suite/.csdp.cache.test-suite Binary files differindex 36efdf469e..5bd4f65546 100644 --- a/test-suite/.csdp.cache.test-suite +++ b/test-suite/.csdp.cache.test-suite diff --git a/test-suite/bugs/closed/bug_13303.v b/test-suite/bugs/closed/bug_13303.v new file mode 100644 index 0000000000..6bee24b48a --- /dev/null +++ b/test-suite/bugs/closed/bug_13303.v @@ -0,0 +1,27 @@ +Module Pt1. + + Module M. Universe i. End M. + Module N. Universe i. End N. + Import M. + Notation foo := Type@{i (* M.i??? *)}. + Import N. + Fail Check foo : Type@{M.i}. (* should NOT succeed *) + Check foo : Type@{i (* N.i *)}. (* should succeed *) + + Definition bar@{i} := Type@{i}. + Check bar : Type@{N.i}. + Check bar : Type@{M.i}. + +End Pt1. + +Module Pt2. + + Module M. Universe i. Notation foo := Type@{i}. End M. + + Definition foo1 := M.foo. + (* should succeed, currently errors undeclared universe i *) + + Definition foo2@{i} : Type@{i} := M.foo. + (* should succeed, currently errors universe inconsistency *) + +End Pt2. diff --git a/test-suite/bugs/closed/bug_13453.v b/test-suite/bugs/closed/bug_13453.v new file mode 100644 index 0000000000..4d0e435df7 --- /dev/null +++ b/test-suite/bugs/closed/bug_13453.v @@ -0,0 +1,6 @@ +Require Extraction. + +Primitive array := #array_type. + +Definition a : array nat := [| 0%nat | 0%nat |]. +Extraction a. diff --git a/test-suite/complexity/bug_13227_1.v b/test-suite/complexity/bug_13227_1.v new file mode 100644 index 0000000000..25aae05217 --- /dev/null +++ b/test-suite/complexity/bug_13227_1.v @@ -0,0 +1,28 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall Y r0 r q q0 r1 q1 : Z, + 3 = 4294967296 * q1 + r1 -> + Y - r1 = 4294967296 * q0 + r0 -> + r1 < 4294967296 -> + 0 <= r1 -> + r0 < 4294967296 -> + 0 <= r0 -> + r < 4 -> + 0 <= r -> + 0 < 4 -> + r0 = 4 * q + r -> + Y < 4294967296 -> + 0 <= Y -> + r = 0 -> + r0 < 268517376 -> + 268513280 <= r0 -> + 268587008 <= Y -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_2.v b/test-suite/complexity/bug_13227_2.v new file mode 100644 index 0000000000..25aae05217 --- /dev/null +++ b/test-suite/complexity/bug_13227_2.v @@ -0,0 +1,28 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall Y r0 r q q0 r1 q1 : Z, + 3 = 4294967296 * q1 + r1 -> + Y - r1 = 4294967296 * q0 + r0 -> + r1 < 4294967296 -> + 0 <= r1 -> + r0 < 4294967296 -> + 0 <= r0 -> + r < 4 -> + 0 <= r -> + 0 < 4 -> + r0 = 4 * q + r -> + Y < 4294967296 -> + 0 <= Y -> + r = 0 -> + r0 < 268517376 -> + 268513280 <= r0 -> + 268587008 <= Y -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_3.v b/test-suite/complexity/bug_13227_3.v new file mode 100644 index 0000000000..707e06e174 --- /dev/null +++ b/test-suite/complexity/bug_13227_3.v @@ -0,0 +1,46 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall (two64 right left : Z) (length_xs v : nat) (x2 x1 : Z) + (length_x : nat) (r3 r2 q r r1 q0 r0 q1 q2 q3 : Z), + two64 = 2 ^ 64 -> + r3 = 8 * Z.of_nat length_xs -> + r2 = 8 * Z.of_nat length_x -> + 0 <= 8 * Z.of_nat length_x -> + 8 * Z.of_nat length_x < two64 -> + r1 = 2 ^ 4 * q + r -> + 0 < 2 ^ 4 -> + 0 <= r -> + r < 2 ^ 4 -> + x1 + q * 2 ^ 3 - x1 = two64 * q0 + r0 -> + 0 < two64 -> + 0 <= r0 -> + r0 < two64 -> + 8 * Z.of_nat length_x = two64 * q1 + r1 -> + 0 <= r1 -> + r1 < two64 -> + x2 - x1 = two64 * q2 + r2 -> + 0 <= r2 -> + r2 < two64 -> + right - left = two64 * q3 + r3 -> + 0 <= r3 -> + r3 < two64 -> + Z.of_nat length_x = Z.of_nat v -> + 0 <= Z.of_nat length_x -> + 0 <= Z.of_nat length_xs -> + 0 <= Z.of_nat v -> + (r2 = 0 -> False) -> + (2 ^ 4 = 0 -> False) -> + (2 ^ 4 < 0 -> False) -> + (two64 = 0 -> False) -> + (two64 < 0 -> False) -> + (r0 < 8 * Z.of_nat length_x -> False) -> + False. +Proof. + intros. + subst. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_4.v b/test-suite/complexity/bug_13227_4.v new file mode 100644 index 0000000000..32cbd4e187 --- /dev/null +++ b/test-suite/complexity/bug_13227_4.v @@ -0,0 +1,45 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall (two64 right left : Z) (length_xs v : nat) (x2 x1 : Z) + (length_x : nat) (r3 r2 q r r1 q0 r0 q1 q2 q3 : Z), + two64 = 2 ^ 64 -> + r3 = 8 * Z.of_nat length_xs -> + r2 = 8 * Z.of_nat length_x -> + 0 <= 8 * Z.of_nat length_x -> + 8 * Z.of_nat length_x < two64 -> + r1 = 2 ^ 4 * q + r -> + 0 < 2 ^ 4 -> + 0 <= r -> + r < 2 ^ 4 -> + x1 + q * 2 ^ 3 - x1 = two64 * q0 + r0 -> + 0 < two64 -> + 0 <= r0 -> + r0 < two64 -> + 8 * Z.of_nat length_x = two64 * q1 + r1 -> + 0 <= r1 -> + r1 < two64 -> + x2 - x1 = two64 * q2 + r2 -> + 0 <= r2 -> + r2 < two64 -> + right - left = two64 * q3 + r3 -> + 0 <= r3 -> + r3 < two64 -> + Z.of_nat length_x = Z.of_nat v -> + 0 <= Z.of_nat length_x -> + 0 <= Z.of_nat length_xs -> + 0 <= Z.of_nat v -> + (r2 = 0 -> False) -> + (2 ^ 4 = 0 -> False) -> + (2 ^ 4 < 0 -> False) -> + (two64 = 0 -> False) -> + (two64 < 0 -> False) -> + (r0 < 8 * Z.of_nat length_x -> False) -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_5.v b/test-suite/complexity/bug_13227_5.v new file mode 100644 index 0000000000..4869c4c6b4 --- /dev/null +++ b/test-suite/complexity/bug_13227_5.v @@ -0,0 +1,79 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +Axiom word: Type. + +(* Expected time < 1.00s *) +Goal forall (right left : Z) (length_xs : nat) (r14 : Z) (v : nat) (x : list word) + (x2 x1 r8 q2 q r q0 r0 r3 r10 r13 q1 r1 r9 r2 r4 q3 q4 + r5 q5 r6 q6 r7 q7 q8 q9 q10 r11 q11 r12 q12 q13 q14 z83 z84 : Z), + z84 = 0 -> + Z.of_nat (Datatypes.length x) - (z83 + 1) <= 0 -> + z84 = Z.of_nat (Datatypes.length x) - (z83 + 1) -> + z83 = 0 -> + q0 <= 0 -> + 0 <= Z.of_nat v -> + 0 <= Z.of_nat length_xs -> + 0 <= Z.of_nat (Datatypes.length x) -> + Z.of_nat (Datatypes.length x) = Z.of_nat v -> + r14 < 2 ^ 64 -> + 0 <= r14 -> + right - left = 2 ^ 64 * q14 + r14 -> + r13 < 2 ^ 64 -> + 0 <= r13 -> + r10 - x1 = 2 ^ 64 * q13 + r13 -> + r12 < 2 ^ 64 -> + 0 <= r12 -> + q = 2 ^ 64 * q12 + r12 -> + r11 < 2 ^ 64 -> + 0 <= r11 -> + r12 * 2 ^ 3 = 2 ^ 64 * q11 + r11 -> + r10 < 2 ^ 64 -> + 0 <= r10 -> + x1 + r11 = 2 ^ 64 * q10 + r10 -> + r9 < 2 ^ 64 -> + 0 <= r9 -> + r10 + r3 = 2 ^ 64 * q9 + r9 -> + r8 < 2 ^ 64 -> + 0 <= r8 -> + x2 - x1 = 2 ^ 64 * q8 + r8 -> + r7 < 2 ^ 64 -> + 0 <= r7 -> + Z.shiftr r8 4 = 2 ^ 64 * q7 + r7 -> + r6 < 2 ^ 64 -> + 0 <= r6 -> + Z.shiftl r7 3 = 2 ^ 64 * q6 + r6 -> + r5 < 2 ^ 64 -> + 0 <= r5 -> + x1 + r6 = 2 ^ 64 * q5 + r5 -> + r4 < 2 ^ 64 -> + 0 <= r4 -> + r5 - x1 = 2 ^ 64 * q4 + r4 -> + r3 < 2 ^ 64 -> + 0 <= r3 -> + 8 = 2 ^ 64 * q3 + r3 -> + r2 < r3 -> + 0 <= r2 -> + r4 = r3 * q2 + r2 -> + r1 < 2 ^ 64 -> + 0 <= r1 -> + 0 < 2 ^ 64 -> + x2 - r9 = 2 ^ 64 * q1 + r1 -> + r0 < r3 -> + 0 <= r0 -> + 0 < r3 -> + r13 = r3 * q0 + r0 -> + r < 2 ^ 4 -> + 0 <= r -> + 0 < 2 ^ 4 -> + r8 = 2 ^ 4 * q + r -> + r8 = 8 * Z.of_nat (Datatypes.length x) -> + r14 = 8 * Z.of_nat length_xs -> + (r1 = 8 * z84 -> False) -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/complexity/bug_13227_6.v b/test-suite/complexity/bug_13227_6.v new file mode 100644 index 0000000000..800aa4f625 --- /dev/null +++ b/test-suite/complexity/bug_13227_6.v @@ -0,0 +1,16 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +(* Expected time < 1.00s *) +Goal forall (x2 x3 x : Z) + (H : 0 <= 1073741824 * x + x2 - 67146752) + (H0 : 0 <= -8192 + x2) + (H1 : 0 <= 34816 + - x2) + (H2 : 0 <= -1073741824 * x - x2 + 1073741823), + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/micromega/bug_13227_1.v b/test-suite/micromega/bug_13227_1.v new file mode 100644 index 0000000000..fa6aa53447 --- /dev/null +++ b/test-suite/micromega/bug_13227_1.v @@ -0,0 +1,75 @@ +Require Import Lia ZArith. +Open Scope Z_scope. + +Unset Lia Cache. + +Axiom word: Type. + +Goal forall (right left : Z) (length_xs : nat) (r14 : Z) (v : nat) + (x : list word) (x2 x1 r8 q2 q r q0 r0 r3 r10 r13 q1 r1 r9 r2 + r4 q3 q4 r5 q5 r6 q6 r7 q7 q8 q9 q10 r11 q11 r12 q12 q13 q14 + z83 z84 : Z), + z84 = Z.of_nat (Datatypes.length x) - (z83 + 1) -> + 0 < Z.of_nat (Datatypes.length x) - (z83 + 1) -> + z83 = 0 -> + q0 <= 0 -> + 0 <= Z.of_nat v -> + 0 <= Z.of_nat length_xs -> + 0 <= Z.of_nat (Datatypes.length x) -> + Z.of_nat (Datatypes.length x) = Z.of_nat v -> + r14 < 2 ^ 64 -> + 0 <= r14 -> + right - left = 2 ^ 64 * q14 + r14 -> + r13 < 2 ^ 64 -> + 0 <= r13 -> + r10 - x1 = 2 ^ 64 * q13 + r13 -> + r12 < 2 ^ 64 -> + 0 <= r12 -> + q = 2 ^ 64 * q12 + r12 -> + r11 < 2 ^ 64 -> + 0 <= r11 -> + r12 * 2 ^ 3 = 2 ^ 64 * q11 + r11 -> + r10 < 2 ^ 64 -> + 0 <= r10 -> + x1 + r11 = 2 ^ 64 * q10 + r10 -> + r9 < 2 ^ 64 -> + 0 <= r9 -> + r10 + r3 = 2 ^ 64 * q9 + r9 -> + r8 < 2 ^ 64 -> + 0 <= r8 -> + x2 - x1 = 2 ^ 64 * q8 + r8 -> + r7 < 2 ^ 64 -> + 0 <= r7 -> + Z.shiftr r8 4 = 2 ^ 64 * q7 + r7 -> + r6 < 2 ^ 64 -> + 0 <= r6 -> + Z.shiftl r7 3 = 2 ^ 64 * q6 + r6 -> + r5 < 2 ^ 64 -> + 0 <= r5 -> + x1 + r6 = 2 ^ 64 * q5 + r5 -> + r4 < 2 ^ 64 -> + 0 <= r4 -> + r5 - x1 = 2 ^ 64 * q4 + r4 -> + r3 < 2 ^ 64 -> + 0 <= r3 -> + 8 = 2 ^ 64 * q3 + r3 -> + r2 < r3 -> + 0 <= r2 -> + r4 = r3 * q2 + r2 -> + r1 < 2 ^ 64 -> + 0 <= r1 -> + 0 < 2 ^ 64 -> + x2 - r9 = 2 ^ 64 * q1 + r1 -> + r0 < r3 -> + 0 <= r0 -> + 0 < r3 -> + r13 = r3 * q0 + r0 -> + r8 = 2 ^ 4 * q + r -> + r8 = 8 * Z.of_nat (Datatypes.length x) -> + r14 = 8 * Z.of_nat length_xs -> + (r1 = 8 * z84 -> False) -> + False. +Proof. + intros. + Time lia. +Qed. diff --git a/test-suite/micromega/int63.v b/test-suite/micromega/int63.v index 20dfa2631e..15146187ca 100644 --- a/test-suite/micromega/int63.v +++ b/test-suite/micromega/int63.v @@ -1,5 +1,6 @@ -Require Import ZArith ZifyInt63 Lia. +Require Import ZArith Lia. Require Import Int63. +Require ZifyInt63. Open Scope int63_scope. diff --git a/test-suite/misc/quotation_token/src/quotation.mlg b/test-suite/misc/quotation_token/src/quotation.mlg index ba0bcb1b3c..0f843b3b14 100644 --- a/test-suite/misc/quotation_token/src/quotation.mlg +++ b/test-suite/misc/quotation_token/src/quotation.mlg @@ -7,6 +7,6 @@ GRAMMAR EXTEND Gram term: LEVEL "0" [ [ s = QUOTATION "foobar:" -> { - CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [GProp,0])) } ] ] + CAst.make ~loc Constrexpr.(CSort Glob_term.(UNamed [CProp,0])) } ] ] ; END diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg index d89ab887a8..bb6eaff409 100644 --- a/test-suite/misc/side-eff-leak-univs/src/evil.mlg +++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg @@ -7,7 +7,7 @@ open Stdarg TACTIC EXTEND magic | [ "magic" ident(i) ident(j) ] -> { - let open Glob_term in - DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() + let open Constrexpr in + DeclareUniv.do_constraint ~poly:false [ CType (Libnames.qualid_of_ident i), Univ.Lt, CType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT() } END diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index df64ae2af3..3477a293e3 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -31,12 +31,6 @@ end : Expr -> Expr [(1 + 1)] : Expr -Let "x" e1 e2 - : expr -Let "x" e1 e2 - : expr -Let "x" e1 e2 : list string - : list string myAnd1 True True : Prop r 2 3 @@ -65,8 +59,6 @@ where |- Type] (pat, p0, p cannot be used) 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: @@ -85,18 +77,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 226, characters 0-160: +File "stdin", line 184, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 239, characters 0-60: +File "stdin", line 197, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 243, characters 0-64: +File "stdin", line 201, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 248, characters 0-62: +File "stdin", line 206, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -105,10 +97,10 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 276, characters 0-61: +File "stdin", line 234, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 280, characters 0-63: +File "stdin", line 238, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] fun x : nat => U (S x) @@ -119,7 +111,7 @@ fun x : nat => V x : forall x : nat, nat * (?T -> ?T) where ?T : [x : nat x0 : ?T |- Type] (x0 cannot be used) -File "stdin", line 297, characters 0-30: +File "stdin", line 255, characters 0-30: Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing] 0 :=: 0 : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index ce488fe18d..ebad12af88 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -79,35 +79,7 @@ Check [1 + 1]. End C. -(* An example of interaction between coercion and notations from - Robbert Krebbers. *) - -Require Import String. - -Module D. - -Inductive expr := - | Var : string -> expr - | Lam : string -> expr -> expr - | App : expr -> expr -> expr. - -Notation Let x e1 e2 := (App (Lam x e2) e1). - -Parameter e1 e2 : expr. - -Check (Let "x" e1 e2). - -Coercion App : expr >-> Funclass. - -Check (Let "x" e1 e2). - -Axiom free_vars :> expr -> list string. - -Check (Let "x" e1 e2) : list string. - -End D. - -(* Fixing bugs reported by G. Gonthier in #9207 *) +(* Fixing overparenthesizing reported by G. Gonthier in #9207 (PR #9214, in 8.10)*) Module I. @@ -152,20 +124,6 @@ Check fun '{|n:=x|} => true. End EmptyRecordSyntax. -Module L. - -(* Testing regression #11053 *) - -Section Test. -Variables (A B : Type) (a : A) (b : B). -Variable c : A -> B. -Coercion c : A >-> B. -Notation COERCION := (c). -Check b = a. -End Test. - -End L. - Module M. (* Accept boxes around the end variables of a recursive notation (if equal boxes) *) diff --git a/test-suite/output/NotationsCoercions.out b/test-suite/output/NotationsCoercions.out new file mode 100644 index 0000000000..56145e5fa5 --- /dev/null +++ b/test-suite/output/NotationsCoercions.out @@ -0,0 +1,22 @@ +Let "x" e1 e2 + : expr +Let "x" e1 e2 + : expr +Let "x" e1 e2 : list string + : list string +b = a + : Prop +foo + : (_ BitVec 32) +#[ r ] 0 + : nat +##[ r ] + : nat +##[ r ] + : nat +#[ r ] 0 + : nat +##[ r ] + : nat +##[ r ] + : nat diff --git a/test-suite/output/NotationsCoercions.v b/test-suite/output/NotationsCoercions.v new file mode 100644 index 0000000000..0524bed98c --- /dev/null +++ b/test-suite/output/NotationsCoercions.v @@ -0,0 +1,77 @@ +(* Tests about skipping a coercion vs using a notation involving a coercion *) + +Require Import String. + +(* Skipping a coercion vs using a notation for the application of the + coercion (from Robbert Krebbers, see PR #8890) *) + +Module A. + +Inductive expr := + | Var : string -> expr + | Lam : string -> expr -> expr + | App : expr -> expr -> expr. + +Notation Let x e1 e2 := (App (Lam x e2) e1). +Parameter e1 e2 : expr. +Check (Let "x" e1 e2). (* always printed the same *) +Coercion App : expr >-> Funclass. +Check (Let "x" e1 e2). (* printed the same from #8890, in 8.10 *) +Axiom free_vars :> expr -> list string. +Check (Let "x" e1 e2) : list string. (* printed the same from #11172, in 8.12 *) + +End A. + +(* Skipping a coercion vs using a notation for the coercion itself + (regression #11053 in 8.10 after PR #8890, addressed by PR #11090) *) + +Module B. + +Section Test. +Variables (A B : Type) (a : A) (b : B). +Variable c : A -> B. +Coercion c : A >-> B. +Notation COERCION := (c). +Check b = a. (* printed the same except in 8.10 *) +End Test. + +End B. + +Module C. + +Record word := { rep: Type }. +Coercion rep : word >-> Sortclass. +Axiom myword: word. +Axiom foo: myword. +Notation "'(_' 'BitVec' '32)'" := (rep myword). +Check foo. (* printed with Bitvec from #8890 in 8.10 and 8.11, regression due to #11172 in 8.12 *) + +End C. + +(* Examples involving coercions to funclass *) + +Module D. + +Record R := { f :> nat -> nat }. +Axiom r : R. +Notation "#[ x ]" := (f x). +Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *) +Notation "##[ x ]" := (f x 0). +Check ##[ r ]. (* printed the same from 8.10 *) +Check #[ r ] 0. (* printed ##[ r ] from 8.10 *) + +End D. + +(* Same examples with a parameter *) + +Module E. + +Record R A := { f :> A -> A }. +Axiom r : R nat. +Notation "#[ x ]" := (f nat x). +Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *) +Notation "##[ x ]" := (f nat x 0). +Check ##[ r ]. (* printed the same from 8.10 *) +Check #[ r ] 0. (* printed ##[ r ] from 8.10 *) + +End E. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d8d3f696b7..0fbb4f4c11 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,61 +1,61 @@ -Inductive Empty@{u} : Type@{u} := -(* u |= *) -Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } -(* u |= *) +Inductive Empty@{uu} : Type@{uu} := +(* uu |= *) +Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A } +(* uu |= *) PWrap has primitive projections with eta conversion. Arguments PWrap _%type_scope Arguments pwrap _%type_scope _ -punwrap@{u} = -fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p - : forall A : Type@{u}, PWrap@{u} A -> A -(* u |= *) +punwrap@{uu} = +fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p + : forall A : Type@{uu}, PWrap@{uu} A -> A +(* uu |= *) Arguments punwrap _%type_scope _ -Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } -(* u |= *) +Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A } +(* uu |= *) Arguments RWrap _%type_scope Arguments rwrap _%type_scope _ -runwrap@{u} = -fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap - : forall A : Type@{u}, RWrap@{u} A -> A -(* u |= *) +runwrap@{uu} = +fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap + : forall A : Type@{uu}, RWrap@{uu} A -> A +(* uu |= *) Arguments runwrap _%type_scope _ -Wrap@{u} = fun A : Type@{u} => A - : Type@{u} -> Type@{u} -(* u |= *) +Wrap@{uu} = fun A : Type@{uu} => A + : Type@{uu} -> Type@{uu} +(* uu |= *) Arguments Wrap _%type_scope -wrap@{u} = -fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap - : forall A : Type@{u}, Wrap@{u} A -> A -(* u |= *) +wrap@{uu} = +fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap + : forall A : Type@{uu}, Wrap@{uu} A -> A +(* uu |= *) Arguments wrap {A}%type_scope {Wrap} -bar@{u} = nat - : Wrap@{u} Set -(* u |= Set < u *) -foo@{u u0 v} = -Type@{u0} -> Type@{v} -> Type@{u} - : Type@{max(u+1,u0+1,v+1)} -(* u u0 v |= *) +bar@{uu} = nat + : Wrap@{uu} Set +(* uu |= Set < uu *) +foo@{uu u v} = +Type@{u} -> Type@{v} -> Type@{uu} + : Type@{max(uu+1,u+1,v+1)} +(* uu u v |= *) Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) = Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) -mono = Type@{mono.u} - : Type@{mono.u+1} -(* {mono.u} |= *) +mono = Type@{mono.uu} + : Type@{mono.uu+1} +(* {mono.uu} |= *) mono - : Type@{mono.u+1} -Type@{mono.u} - : Type@{mono.u+1} + : Type@{mono.uu+1} +Type@{mono.uu} + : Type@{mono.uu+1} The command has indeed failed with message: -Universe u already exists. +Universe uu already exists. monomono : Type@{MONOU+1} mono.monomono @@ -63,23 +63,23 @@ mono.monomono monomono : Type@{MONOU+1} mono - : Type@{mono.u+1} + : Type@{mono.uu+1} The command has indeed failed with message: -Universe u already exists. +Universe uu already exists. bobmorane = let tt := Type@{UnivBinders.32} in let ff := Type@{UnivBinders.34} in tt -> ff : Type@{max(UnivBinders.31,UnivBinders.33)} The command has indeed failed with message: -Universe u already bound. +Universe uu already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) -foo@{u u0 v} = -Type@{u0} -> Type@{v} -> Type@{u} - : Type@{max(u+1,u0+1,v+1)} -(* u u0 v |= *) +foo@{uu u v} = +Type@{u} -> Type@{v} -> Type@{uu} + : Type@{max(uu+1,u+1,v+1)} +(* uu u v |= *) Inductive Empty@{E} : Type@{E} := (* E |= *) Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } @@ -103,45 +103,38 @@ The command has indeed failed with message: This object does not support universe names. The command has indeed failed with message: Cannot enforce v < u because u < gU < gV < v -bind_univs.mono = -Type@{bind_univs.mono.u} - : Type@{bind_univs.mono.u+1} -(* {bind_univs.mono.u} |= *) -bind_univs.poly@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -insec@{v} = Type@{u} -> Type@{v} - : Type@{max(u+1,v+1)} +insec@{v} = Type@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} (* v |= *) Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} (* k |= *) Arguments inseccstr _%type_scope -insec@{u v} = Type@{u} -> Type@{v} - : Type@{max(u+1,v+1)} -(* u v |= *) -Inductive insecind@{u k} : Type@{k+1} := - inseccstr : Type@{k} -> insecind@{u k} -(* u k |= *) +insec@{uu v} = Type@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} +(* uu v |= *) +Inductive insecind@{uu k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{uu k} +(* uu k |= *) Arguments inseccstr _%type_scope insec2@{u} = Prop : Type@{Set+1} (* u |= *) -inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -SomeMod.inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -inmod@{u} = Type@{u} - : Type@{u+1} -(* u |= *) -Applied.infunct@{u v} = -inmod@{u} -> Type@{v} - : Type@{max(u+1,v+1)} -(* u v |= *) +inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +SomeMod.inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +inmod@{uu} = Type@{uu} + : Type@{uu+1} +(* uu |= *) +Applied.infunct@{uu v} = +inmod@{uu} -> Type@{v} + : Type@{max(uu+1,v+1)} +(* uu v |= *) axfoo@{i u u0} : Type@{u} -> Type@{i} (* i u u0 |= *) @@ -166,3 +159,13 @@ Arguments axbar' _%type_scope Expands to: Constant UnivBinders.axbar' The command has indeed failed with message: When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). +foo@{i} = Type@{M.i} -> Type@{i} + : Type@{max(M.i+1,i+1)} +(* i |= *) +bind_univs.mono = +Type@{bind_univs.mono.u} + : Type@{bind_univs.mono.u+1} +(* {bind_univs.mono.u} |= *) +bind_univs.poly@{u} = Type@{u} + : Type@{u+1} +(* u |= *) diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 582a5e969a..ed6e90b2a6 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -5,32 +5,32 @@ Set Printing Universes. (* Unset Strict Universe Declaration. *) (* universe binders on inductive types and record projections *) -Inductive Empty@{u} : Type@{u} := . +Inductive Empty@{uu} : Type@{uu} := . Print Empty. Set Primitive Projections. -Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }. +Record PWrap@{uu} (A:Type@{uu}) := pwrap { punwrap : A }. Print PWrap. Print punwrap. Unset Primitive Projections. -Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }. +Record RWrap@{uu} (A:Type@{uu}) := rwrap { runwrap : A }. Print RWrap. Print runwrap. (* universe binders also go on the constants for operational typeclasses. *) -Class Wrap@{u} (A:Type@{u}) := wrap : A. +Class Wrap@{uu} (A:Type@{uu}) := wrap : A. Print Wrap. Print wrap. (* Instance in lemma mode used to ignore the binders. *) -Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed. +Instance bar@{uu} : Wrap@{uu} Set. Proof. exact nat. Qed. Print bar. Unset Strict Universe Declaration. (* The universes in the binder come first, then the extra universes in order of appearance. *) -Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. +Definition foo@{uu +} := Type -> Type@{v} -> Type@{uu}. Print foo. Check Type@{i} -> Type@{j}. @@ -40,13 +40,13 @@ Eval cbv in Type@{i} -> Type@{j}. Set Strict Universe Declaration. (* Binders even work with monomorphic definitions! *) -Monomorphic Definition mono@{u} := Type@{u}. +Monomorphic Definition mono@{uu} := Type@{uu}. Print mono. Check mono. -Check Type@{mono.u}. +Check Type@{mono.uu}. Module mono. - Fail Monomorphic Universe u. + Fail Monomorphic Universe uu. Monomorphic Universe MONOU. Monomorphic Definition monomono := Type@{MONOU}. @@ -60,28 +60,28 @@ Import mono. Check monomono. (* unqualified MONOU *) Check mono. (* still qualified mono.u *) -Monomorphic Constraint Set < UnivBinders.mono.u. +Monomorphic Constraint Set < UnivBinders.mono.uu. Module mono2. - Monomorphic Universe u. + Monomorphic Universe uu. End mono2. -Fail Monomorphic Definition mono2@{u} := Type@{u}. +Fail Monomorphic Definition mono2@{uu} := Type@{uu}. Module SecLet. Unset Universe Polymorphism. Section foo. - (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) + (* Fail Let foo@{} := Type@{uu}. (* doesn't parse: Let foo@{...} doesn't exist *) *) Unset Strict Universe Declaration. - Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) - Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *) + Let tt : Type@{uu} := Type@{v}. (* names disappear in the ether *) + Let ff : Type@{uu}. Proof. exact Type@{v}. Qed. (* names disappear into space *) Definition bobmorane := tt -> ff. End foo. Print bobmorane. End SecLet. (* fun x x => foo is nonsense with local binders *) -Fail Definition fo@{u u} := Type@{u}. +Fail Definition fo@{uu uu} := Type@{uu}. (* Using local binders for printing. *) Print foo@{E M N}. @@ -106,14 +106,9 @@ Fail Print Coq.Init.Logic@{E}. Monomorphic Universes gU gV. Monomorphic Constraint gU < gV. Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat. -(* Universe binders survive through compilation, sections and modules. *) -Require TestSuite.bind_univs. -Print bind_univs.mono. -Print bind_univs.poly. - Section SomeSec. - Universe u. - Definition insec@{v} := Type@{u} -> Type@{v}. + Universe uu. + Definition insec@{v} := Type@{uu} -> Type@{v}. Print insec. Inductive insecind@{k} := inseccstr : Type@{k} -> insecind. @@ -129,7 +124,7 @@ End SomeSec2. Print insec2. Module SomeMod. - Definition inmod@{u} := Type@{u}. + Definition inmod@{uu} := Type@{uu}. Print inmod. End SomeMod. Print SomeMod.inmod. @@ -138,7 +133,7 @@ Print inmod. Module Type SomeTyp. Definition inmod := Type. End SomeTyp. Module SomeFunct (In : SomeTyp). - Definition infunct@{u v} := In.inmod@{u} -> Type@{v}. + Definition infunct@{uu v} := In.inmod@{uu} -> Type@{v}. End SomeFunct. Module Applied := SomeFunct(SomeMod). Print Applied.infunct. @@ -147,7 +142,7 @@ Print Applied.infunct. In polymorphic mode the domain Type gets separate universes for the different axioms, but all axioms have to declare all universes. In - polymorphic mode they get the same universes, ie the type is only + monomorphic mode they get the same universes, ie the type is only interpd once. *) Axiom axfoo@{i+} axbar : Type -> Type@{i}. Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. @@ -155,3 +150,18 @@ Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. About axfoo. About axbar. About axfoo'. About axbar'. Fail Axiom failfoo failbar@{i} : Type. + +(* Notation interaction *) +Module Notas. + Unset Universe Polymorphism. + Module Import M. Universe i. End M. + + Polymorphic Definition foo@{i} := Type@{M.i} -> Type@{i}. + Print foo. (* must not print Type@{i} -> Type@{i} *) + +End Notas. + +(* Universe binders survive through compilation, sections and modules. *) +Require TestSuite.bind_univs. +Print bind_univs.mono. +Print bind_univs.poly. diff --git a/test-suite/ssr/ipat_dup.v b/test-suite/ssr/ipat_dup.v index b1936df31d..61666959c4 100644 --- a/test-suite/ssr/ipat_dup.v +++ b/test-suite/ssr/ipat_dup.v @@ -2,6 +2,8 @@ Require Import ssreflect. Section Dup. +Section withP. + Variable P : nat -> Prop. Lemma test_dup1 : forall n : nat, P n. @@ -10,4 +12,18 @@ Proof. move=> /[dup] m n; suff: P n by []. Abort. Lemma test_dup2 : let n := 1 in False. Proof. move=> /[dup] m n; have : m = n := eq_refl. Abort. +End withP. + +Lemma test_dup_plus P Q : P -> Q -> False. +Proof. +move=> + /[dup] q. +suff: P -> Q -> False by []. +Abort. + +Lemma test_dup_plus2 P : P -> let x := 0 in False. +Proof. +move=> + /[dup] y. +suff: P -> let x := 0 in False by []. +Abort. + End Dup. diff --git a/test-suite/ssr/ipat_swap.v b/test-suite/ssr/ipat_swap.v index 1d78a2a009..a06dae1264 100644 --- a/test-suite/ssr/ipat_swap.v +++ b/test-suite/ssr/ipat_swap.v @@ -7,7 +7,19 @@ Definition P n := match n with 1 => true | _ => false end. Lemma test_swap1 : forall (n : nat) (b : bool), P n = b. Proof. move=> /[swap] b n; suff: P n = b by []. Abort. -Lemma test_swap1 : let n := 1 in let b := true in False. +Lemma test_swap2 : let n := 1 in let b := true in False. Proof. move=> /[swap] b n; have : P n = b := eq_refl. Abort. +Lemma test_swap_plus P Q R : P -> Q -> R -> False. +Proof. +move=> + /[swap]. +suff: P -> R -> Q -> False by []. +Abort. + +Lemma test_swap_plus2 P : P -> let x := 0 in let y := 1 in False. +Proof. +move=> + /[swap]. +suff: P -> let y := 1 in let x := 0 in False by []. +Abort. + End Swap. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 97b4e39168..f1dad301fd 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.13") -*- *) +(* -*- coq-prog-args: ("-compat" "8.14") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq813. +Import Coq.Compat.Coq814. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index c06dd6e450..a737e0c98e 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(* -*- coq-prog-args: ("-compat" "8.12") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. Import Coq.Compat.Coq812. -Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..f4cf703ec7 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.11") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. +Import Coq.Compat.Coq813. +Import Coq.Compat.Coq812. +Import Coq.Compat.Coq811. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 83010f2149..07d5fcd3ab 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.12") -*- *) +(* -*- coq-prog-args: ("-compat" "8.13") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq814. Import Coq.Compat.Coq813. -Import Coq.Compat.Coq812. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 253b48e4d9..2308656f7c 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -426,3 +426,12 @@ Abort. (* (reported as bug #7356) *) Check fun (P : nat -> Prop) (x:nat) (h:P x) => exist _ ?[z] (h : P ?z). + +(* A printing check in passing *) + +Axiom abs : forall T, T. +Fail Type let x := _ in + ltac:( + let t := type of x in + unify x (abs t); + exact 0). diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 7ff5571ffb..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 --release || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? |