diff options
Diffstat (limited to 'test-suite')
23 files changed, 682 insertions, 63 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index f169f86e8..6865dcc76 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -95,7 +95,8 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile PREREQUISITELOG = prerequisite/admit.v.log \ - prerequisite/make_local.v.log prerequisite/make_notation.v.log + prerequisite/make_local.v.log prerequisite/make_notation.v.log \ + prerequisite/bind_univs.v.log ####################################################################### # Phony targets diff --git a/test-suite/bugs/closed/3125.v b/test-suite/bugs/closed/3125.v new file mode 100644 index 000000000..797146174 --- /dev/null +++ b/test-suite/bugs/closed/3125.v @@ -0,0 +1,27 @@ +(* Not considering singleton template-polymorphic inductive types as + propositions for injection/inversion *) + +(* This is also #4560 and #6273 *) + +Inductive foo := foo_1. + +Goal forall (a b : foo), Some a = Some b -> a = b. +Proof. + intros a b H. + inversion H. + reflexivity. +Qed. + +(* Check that Prop is not concerned *) + +Inductive bar : Prop := bar_1. + +Goal + forall (a b : bar), + Some a = Some b -> + a = b. +Proof. + intros a b H. + inversion H. + Fail reflexivity. +Abort. diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v index da12b6868..5210b2703 100644 --- a/test-suite/bugs/closed/3559.v +++ b/test-suite/bugs/closed/3559.v @@ -65,6 +65,7 @@ Axiom path_iff_hprop_uncurried : forall `{IsHProp A, IsHProp B}, (A <-> B) -> A = B. Inductive V : Type@{U'} := | set {A : Type@{U}} (f : A -> V) : V. Axiom is0trunc_V : IsTrunc (trunc_S (trunc_S minus_two)) V. +Existing Instance is0trunc_V. Axiom bisimulation : V@{U' U} -> V@{U' U} -> hProp@{U'}. Axiom bisimulation_refl : forall (v : V), bisimulation v v. Axiom bisimulation_eq : forall (u v : V), bisimulation u v -> u = v. diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index fd9640b89..fa30132ab 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -3,49 +3,44 @@ Set Printing Universes. Set Universe Polymorphism. Definition foo (a := Type) (b := Type) (c := Type) := Type. Print foo. -(* foo = -let a := Type@{Top.1} in -let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4} - : Type@{Top.4+1} -(* Top.1 - Top.2 - Top.3 - Top.4 |= *) *) -Check @foo. (* foo@{Top.5 Top.6 Top.7 -Top.8} - : Type@{Top.8+1} -(* Top.5 - Top.6 - Top.7 - Top.8 |= *) *) +(* foo@{Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10} = +let a := Type@{Top.2} in let b := Type@{Top.5} in let c := Type@{Top.8} in Type@{Top.10} + : Type@{Top.10+1} +(* Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10 |= Top.2 < Top.3 + Top.5 < Top.6 + Top.8 < Top.9 + *) + *) +Check @foo. (* foo@{Top.11 Top.12 Top.13 Top.14 Top.15 Top.16 +Top.17} + : Type@{Top.17+1} +(* Top.11 Top.12 Top.13 Top.14 Top.15 Top.16 Top.17 |= Top.11 < Top.12 + Top.13 < Top.14 + Top.15 < Top.16 + *) + *) Definition bar := ltac:(let t := eval compute in foo in exact t). -Check @bar. (* bar@{Top.13 Top.14 Top.15 -Top.16} - : Type@{Top.16+1} -(* Top.13 - Top.14 - Top.15 - Top.16 |= *) *) -(* The following should fail, since [bar] should only need one universe. *) -Check @bar@{i j}. +Check @bar. (* bar@{Top.27} + : Type@{Top.27+1} +(* Top.27 |= *) *) + +Check @bar@{i}. Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c. Definition qux := Eval compute in baz. -Check @qux. (* qux@{Top.24 Top.25 -Top.26} - : Type@{max(Top.24+1, Top.26+1)} -(* Top.24 - Top.25 - Top.26 |= Top.25 < Top.24 - Top.26 < Top.25 - *) *) -Print qux. (* qux = -Type@{Top.21} -> Type@{Top.23} - : Type@{max(Top.21+1, Top.23+1)} -(* Top.21 - Top.22 - Top.23 |= Top.22 < Top.21 - Top.23 < Top.22 - *) *) +Check @qux. (* qux@{Top.38 Top.39 Top.40 +Top.41} + : Type@{max(Top.38+1, Top.41+1)} +(* Top.38 Top.39 Top.40 Top.41 |= Top.38 < Top.39 + Top.40 < Top.38 + Top.41 < Top.40 + *) *) +Print qux. (* qux@{Top.34 Top.35 Top.36 Top.37} = +Type@{Top.34} -> Type@{Top.37} + : Type@{max(Top.34+1, Top.37+1)} +(* Top.34 Top.35 Top.36 Top.37 |= Top.34 < Top.35 + Top.36 < Top.34 + Top.37 < Top.36 + *) *) Fail Check @qux@{Set Set}. Check @qux@{Type Type Type Type}. (* [qux] should only need two universes *) diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v index a96a13700..c069b2d9d 100644 --- a/test-suite/bugs/closed/4390.v +++ b/test-suite/bugs/closed/4390.v @@ -8,16 +8,16 @@ Universe i. End foo. End M. -Check Type@{i}. +Check Type@{M.i}. (* Succeeds *) Fail Check Type@{j}. (* Error: Undeclared universe: j *) -Definition foo@{j} : Type@{i} := Type@{j}. +Definition foo@{j} : Type@{M.i} := Type@{j}. (* ok *) End A. - +Import A. Import M. Set Universe Polymorphism. Fail Universes j. Monomorphic Universe j. diff --git a/test-suite/bugs/closed/5347.v b/test-suite/bugs/closed/5347.v new file mode 100644 index 000000000..9267b3eb6 --- /dev/null +++ b/test-suite/bugs/closed/5347.v @@ -0,0 +1,10 @@ +Set Universe Polymorphism. + +Axiom X : Type. +(* Used to declare [x0@{u1 u2} : X@{u1}] and [x1@{} : X@{u2}] leaving + the type of x1 with undeclared universes. After PR #891 this should + error at declaration time. *) +Axiom x₀ x₁ : X. +Axiom Xᵢ : X -> Type. + +Check Xᵢ x₁. (* conversion test raised anomaly universe undefined *) diff --git a/test-suite/bugs/closed/5717.v b/test-suite/bugs/closed/5717.v new file mode 100644 index 000000000..1bfd917d2 --- /dev/null +++ b/test-suite/bugs/closed/5717.v @@ -0,0 +1,5 @@ +Definition foo@{i} (A : Type@{i}) (l : list A) := + match l with + | nil => nil + | cons _ t => t + end. diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v index b4c745375..d02a5f120 100644 --- a/test-suite/bugs/closed/HoTT_coq_064.v +++ b/test-suite/bugs/closed/HoTT_coq_064.v @@ -178,6 +178,7 @@ Definition IsColimit `{Funext} C D (F : Functor D C) Generalizable All Variables. Axiom fs : Funext. +Existing Instance fs. Section bar. diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh index 378573957..e48f704a2 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-fail/run.sh @@ -10,7 +10,7 @@ cat > _CoqProject <<EOT ./src/test.mli EOT -mkdir src +mkdir -p src cat > src/test_plugin.mllib <<EOT Test diff --git a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh index 1b57a356b..4a8f58655 100755 --- a/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh +++ b/test-suite/coq-makefile/plugin-reach-outside-API-and-succeed-by-bypassing-the-API/run.sh @@ -11,7 +11,7 @@ cat > _CoqProject <<EOT ./src/test.mli EOT -mkdir src +mkdir -p src cat > src/test_plugin.mllib <<EOT Test diff --git a/test-suite/output/Extraction_infix.out b/test-suite/output/Extraction_infix.out new file mode 100644 index 000000000..29d50775a --- /dev/null +++ b/test-suite/output/Extraction_infix.out @@ -0,0 +1,20 @@ +(** val test : foo **) + +let test = + (fun (b, p) -> bar) (True, False) +(** val test : foo **) + +let test = + True@@?False +(** val test : foo **) + +let test = + True#^^False +(** val test : foo **) + +let test = + True@?:::False +(** val test : foo **) + +let test = + True @?::: False diff --git a/test-suite/output/Extraction_infix.v b/test-suite/output/Extraction_infix.v new file mode 100644 index 000000000..fe5926a36 --- /dev/null +++ b/test-suite/output/Extraction_infix.v @@ -0,0 +1,26 @@ +(* @herbelin's example for issue #6212 *) + +Require Import Extraction. +Inductive I := C : bool -> bool -> I. +Definition test := C true false. + +(* the parentheses around the function wrong signalled an infix operator *) + +Extract Inductive I => "foo" [ "(fun (b, p) -> bar)" ]. +Extraction test. + +(* some bonafide infix operators *) + +Extract Inductive I => "foo" [ "(@@?)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(#^^)" ]. +Extraction test. + +Extract Inductive I => "foo" [ "(@?:::)" ]. +Extraction test. + +(* allow whitespace around infix operator *) + +Extract Inductive I => "foo" [ "( @?::: )" ]. +Extraction test. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index ecb8d2c9f..a1028bda0 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -84,3 +84,9 @@ a≡ : Set .α : Set +# a : .α => +# b : .α => +let res := 0 in +for i from 0 to a updating (res) +{{for j from 0 to b updating (res) {{S res}};; res}};; res + : .α -> .α -> .α diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 0dcb74652..4c3eaa0c7 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -146,3 +146,24 @@ Check .a≡. Notation ".α" := nat. Check nat. Check .α. + +(* A test for #6304 *) + +Module M6304. +Notation "'for' m 'from' 0 'to' N 'updating' ( s1 ) {{ b }} ;; rest" := + (let s1 := + (fix rec(n: nat) := match n with + | 0 => s1 + | S m => let s1 := rec m in b + end) N + in rest) + (at level 20). + +Check fun (a b : nat) => + let res := 0 in + for i from 0 to a updating (res) {{ + for j from 0 to b updating (res) {{ S res }};; + res + }};; res. + +End M6304. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 904ff68aa..d6d410d1a 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,12 +1,175 @@ +NonCumulative Inductive Empty@{u} : Type@{u} := +NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } + +PWrap has primitive projections with eta conversion. +For PWrap: Argument scope is [type_scope] +For pwrap: Argument scopes are [type_scope _] +punwrap@{u} = +fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p + : forall A : Type@{u}, PWrap@{u} A -> A +(* u |= *) + +punwrap is universe polymorphic +Argument scopes are [type_scope _] +NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } + +For RWrap: Argument scope is [type_scope] +For rwrap: Argument scopes are [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 is universe polymorphic +Argument scopes are [type_scope _] +Wrap@{u} = fun A : Type@{u} => A + : Type@{u} -> Type@{u} +(* u |= *) + +Wrap is universe polymorphic +Argument scope is [type_scope] +wrap@{u} = +fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap + : forall A : Type@{u}, Wrap@{u} A -> A +(* u |= *) + +wrap is universe polymorphic +Arguments A, Wrap are implicit and maximally inserted +Argument scopes are [type_scope _] bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) bar is universe polymorphic -foo@{u Top.8 v} = -Type@{Top.8} -> Type@{v} -> Type@{u} - : Type@{max(u+1, Top.8+1, v+1)} -(* u Top.8 v |= *) +foo@{u Top.17 v} = +Type@{Top.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1,Top.17+1,v+1)} +(* u Top.17 v |= *) foo is universe polymorphic +Monomorphic mono = Type@{mono.u} + : Type@{mono.u+1} +(* {mono.u} |= *) + +mono is not universe polymorphic +mono + : Type@{mono.u+1} +Type@{mono.u} + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +monomono + : Type@{MONOU+1} +mono.monomono + : Type@{mono.MONOU+1} +monomono + : Type@{MONOU+1} +mono + : Type@{mono.u+1} +The command has indeed failed with message: +Universe u already exists. +bobmorane = +let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff + : Type@{max(tt.u,ff.u)} +The command has indeed failed with message: +Universe u already bound. +foo@{E M N} = +Type@{M} -> Type@{N} -> Type@{E} + : Type@{max(E+1,M+1,N+1)} +(* E M N |= *) + +foo is universe polymorphic +foo@{Top.16 Top.17 Top.18} = +Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16} + : Type@{max(Top.16+1,Top.17+1,Top.18+1)} +(* Top.16 Top.17 Top.18 |= *) + +foo is universe polymorphic +NonCumulative Inductive Empty@{E} : Type@{E} := +NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } + +PWrap has primitive projections with eta conversion. +For PWrap: Argument scope is [type_scope] +For pwrap: Argument scopes are [type_scope _] +punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A +(* K |= *) + +punwrap is universe polymorphic +Argument scopes are [type_scope _] +punwrap is transparent +Expands to: Constant Top.punwrap +The command has indeed failed with message: +Universe instance should have length 3 +The command has indeed failed with message: +Universe instance should have length 0 +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 +Monomorphic bind_univs.mono = +Type@{bind_univs.mono.u} + : Type@{bind_univs.mono.u+1} +(* {bind_univs.mono.u} |= *) + +bind_univs.mono is not universe polymorphic +bind_univs.poly@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +bind_univs.poly is universe polymorphic +insec@{v} = Type@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* v |= *) + +insec is universe polymorphic +insec@{u v} = Type@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* u v |= *) + +insec is universe polymorphic +inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +inmod is universe polymorphic +SomeMod.inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +SomeMod.inmod is universe polymorphic +inmod@{u} = Type@{u} + : Type@{u+1} +(* u |= *) + +inmod is universe polymorphic +Applied.infunct@{u v} = +inmod@{u} -> Type@{v} + : Type@{max(u+1,v+1)} +(* u v |= *) + +Applied.infunct is universe polymorphic +axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i} +(* i Top.41 Top.42 |= *) + +axfoo is universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axfoo +axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i} +(* i Top.41 Top.42 |= *) + +axbar is universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axbar +axfoo' : Type@{Top.44} -> Type@{axbar'.i} + +axfoo' is not universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.axfoo' +axbar' : Type@{Top.44} -> Type@{axbar'.i} + +axbar' is not universe polymorphic +Argument scope is [type_scope] +Expands to: Constant Top.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). diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 8656ff1a3..266d94ad9 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,13 +1,146 @@ Set Universe Polymorphism. Set Printing Universes. -Unset Strict Universe Declaration. +(* Unset Strict Universe Declaration. *) + +(* universe binders on inductive types and record projections *) +Inductive Empty@{u} : Type@{u} := . +Print Empty. + +Set Primitive Projections. +Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }. +Print PWrap. +Print punwrap. + +Unset Primitive Projections. +Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }. +Print RWrap. +Print runwrap. -Class Wrap A := wrap : A. +(* universe binders also go on the constants for operational typeclasses. *) +Class Wrap@{u} (A:Type@{u}) := wrap : A. +Print Wrap. +Print wrap. -Instance bar@{u} : Wrap@{u} Set. Proof nat. +(* Instance in lemma mode used to ignore the binders. *) +Instance bar@{u} : Wrap@{u} 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}. Print foo. +Set Strict Universe Declaration. + +(* Binders even work with monomorphic definitions! *) +Monomorphic Definition mono@{u} := Type@{u}. +Print mono. +Check mono. +Check Type@{mono.u}. + +Module mono. + Fail Monomorphic Universe u. + Monomorphic Universe MONOU. + + Monomorphic Definition monomono := Type@{MONOU}. + Check monomono. +End mono. +Check mono.monomono. (* qualified MONOU *) +Import mono. +Check monomono. (* unqualified MONOU *) +Check mono. (* still qualified mono.u *) + +Monomorphic Constraint Set < Top.mono.u. + +Module mono2. + Monomorphic Universe u. +End mono2. + +Fail Monomorphic Definition mono2@{u} := Type@{u}. + +Module SecLet. + Unset Universe Polymorphism. + Section foo. + (* Fail Let foo@{} := Type@{u}. (* 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. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *) + Definition bobmorane := tt -> ff. + End foo. + Print bobmorane. (* + bobmorane@{Top.15 Top.16 ff.u ff.v} = + let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff + : Type@{max(Top.15,ff.u)} + (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15 + ff.v < ff.u + *) + + bobmorane is universe polymorphic + *) +End SecLet. + +(* fun x x => foo is nonsense with local binders *) +Fail Definition fo@{u u} := Type@{u}. + +(* Using local binders for printing. *) +Print foo@{E M N}. +(* Underscores discard the name if there's one. *) +Print foo@{_ _ _}. + +(* Also works for inductives and records. *) +Print Empty@{E}. +Print PWrap@{E}. + +(* Also works for About. *) +About punwrap@{K}. + +(* Instance length check. *) +Fail Print foo@{E}. +Fail Print mono@{E}. + +(* Not everything can be printed with custom universe names. *) +Fail Print Coq.Init.Logic@{E}. + +(* Nice error when constraints are impossible. *) +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}. + Print insec. +End SomeSec. +Print insec. + +Module SomeMod. + Definition inmod@{u} := Type@{u}. + Print inmod. +End SomeMod. +Print SomeMod.inmod. +Import SomeMod. +Print inmod. + +Module Type SomeTyp. Definition inmod := Type. End SomeTyp. +Module SomeFunct (In : SomeTyp). + Definition infunct@{u v} := In.inmod@{u} -> Type@{v}. +End SomeFunct. +Module Applied := SomeFunct(SomeMod). +Print Applied.infunct. + +(* Multi-axiom declaration + + 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 + interpd once. *) +Axiom axfoo@{i+} axbar : Type -> Type@{i}. +Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}. + +About axfoo. About axbar. About axfoo'. About axbar'. + +Fail Axiom failfoo failbar@{i} : Type. diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 172612405..7326f137c 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,20 +1,40 @@ The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.foo" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.bar" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing arguments for variables y and _. +The user-defined tactic "Top.bar" was not fully applied: +There are missing arguments for variables y and _, +an argument was provided for variable x. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.baz" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.qux" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +The user-defined tactic "Top.mydo" was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable _. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable _, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +The user-defined tactic "Top.rec" was not fully applied: +There is a missing argument for variable x, +no arguments at all were provided. The command has indeed failed with message: -A fully applied tactic is expected: missing argument for variable x. +An unnamed user-defined tactic was not fully applied: +There is a missing argument for variable x, +an argument was provided for variable tac. diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v new file mode 100644 index 000000000..e834fde11 --- /dev/null +++ b/test-suite/prerequisite/bind_univs.v @@ -0,0 +1,7 @@ +(* Used in output/UnivBinders.v *) + +Monomorphic Definition mono@{u} := Type@{u}. + +Polymorphic Definition poly@{u} := Type@{u}. + +Monomorphic Universe reqU. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index e3f90f6d9..3c0ad2070 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -147,3 +147,9 @@ Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x Fail Check {x@{u},y|x=x}. Fail Check {?[n],y|0=0}. + +(* Check that 10 is well declared left associative *) + +Section C. +Notation "f $$$ x" := (id f x) (at level 10, left associativity). +End C. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 6b1f0315b..cd6eac35c 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -240,3 +240,20 @@ Module IterativeDeepening. Qed. End IterativeDeepening. + +Module AxiomsAreInstances. + Set Typeclasses Axioms Are Instances. + Class TestClass1 := {}. + Axiom testax1 : TestClass1. + Definition testdef1 : TestClass1 := _. + + Unset Typeclasses Axioms Are Instances. + Class TestClass2 := {}. + Axiom testax2 : TestClass2. + Fail Definition testdef2 : TestClass2 := _. + + (* we didn't break typeclasses *) + Existing Instance testax2. + Definition testdef2 : TestClass2 := _. + +End AxiomsAreInstances. diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index 3178c6fc1..730b367d6 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -55,6 +55,7 @@ Module Backtracking. Axiom A : Type. Existing Class A. Axioms a b c d e: A. + Existing Instances a b c d e. Ltac get_value H := eval cbv delta [H] in H. diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 7eaafc354..d76b30791 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -190,6 +190,8 @@ Module binders. Fail Defined. Abort. + Fail Lemma bar@{u v | } : let x := (fun x => x) : Type@{u} -> Type@{v} in nat. + Lemma bar@{i j| i < j} : Type@{j}. Proof. exact Type@{i}. @@ -200,6 +202,10 @@ Module binders. exact Type@{i}. Qed. + Monomorphic Universe M. + Fail Definition with_mono@{u|} : Type@{M} := Type@{u}. + Definition with_mono@{u|u < M} : Type@{M} := Type@{u}. + End binders. Section cats. @@ -399,6 +405,31 @@ Module Anonymous. End Anonymous. +Module Restrict. + (* Universes which don't appear in the term should be pruned, unless they have names *) + Set Universe Polymorphism. + + Ltac exact0 := let x := constr:(Type) in exact 0. + Definition dummy_pruned@{} : nat := ltac:(exact0). + + Definition named_not_pruned@{u} : nat := 0. + Check named_not_pruned@{_}. + + Definition named_not_pruned_nonstrict : nat := ltac:(let x := constr:(Type@{u}) in exact 0). + Check named_not_pruned_nonstrict@{_}. + + Lemma lemma_restrict_poly@{} : nat. + Proof. exact0. Defined. + + Unset Universe Polymorphism. + Lemma lemma_restrict_mono_qed@{} : nat. + Proof. exact0. Qed. + + Lemma lemma_restrict_abstract@{} : nat. + Proof. abstract exact0. Qed. + +End Restrict. + Module F. Context {A B : Type}. Definition foo : Type := B. @@ -430,3 +461,10 @@ Section test_letin_subtyping. Qed. End test_letin_subtyping. + +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@{_ _ _ _ _ _ _ _}. +End ObligationRegression. diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v new file mode 100644 index 000000000..c4a1d7c28 --- /dev/null +++ b/test-suite/success/unidecls.v @@ -0,0 +1,121 @@ +Set Printing Universes. + +Module unidecls. + Universes a b. +End unidecls. + +Universe a. + +Constraint a < unidecls.a. + +Print Universes. + +(** These are different universes *) +Check Type@{a}. +Check Type@{unidecls.a}. + +Check Type@{unidecls.b}. + +Fail Check Type@{unidecls.c}. + +Fail Check Type@{i}. +Universe foo. +Module Foo. + (** Already declared globaly: but universe names are scoped at the module level *) + Universe foo. + Universe bar. + + Check Type@{Foo.foo}. + Definition bar := 0. +End Foo. + +(** Already declared in the module *) +Universe bar. + +(** Accessible outside the module: universe declarations are global *) +Check Type@{bar}. +Check Type@{Foo.bar}. + +Check Type@{Foo.foo}. +(** The same *) +Check Type@{foo}. +Check Type@{Top.foo}. + +Universe secfoo. +Section Foo'. + Fail Universe secfoo. + Universe secfoo2. + Check Type@{Foo'.secfoo2}. + Constraint secfoo2 < a. +End Foo'. + +Check Type@{secfoo2}. +Fail Check Type@{Foo'.secfoo2}. +Fail Check eq_refl : Type@{secfoo2} = Type@{a}. + +(** Below, u and v are global, fixed universes *) +Module Type Arg. + Universe u. + Parameter T: Type@{u}. +End Arg. + +Module Fn(A : Arg). + Universes v. + + Check Type@{A.u}. + Constraint A.u < v. + + Definition foo : Type@{v} := nat. + Definition bar : Type@{A.u} := nat. + + Fail Definition foo(A : Type@{v}) : Type@{A.u} := A. +End Fn. + +Module ArgImpl : Arg. + Definition T := nat. +End ArgImpl. + +Module ArgImpl2 : Arg. + Definition T := bool. +End ArgImpl2. + +(** Two applications of the functor result in the exact same universes *) +Module FnApp := Fn(ArgImpl). + +Check Type@{FnApp.v}. +Check FnApp.foo. +Check FnApp.bar. + +Check (eq_refl : Type@{ArgImpl.u} = Type@{ArgImpl2.u}). + +Module FnApp2 := Fn(ArgImpl). +Check Type@{FnApp2.v}. +Check FnApp2.foo. +Check FnApp2.bar. + +Import ArgImpl2. +(** Now u refers to ArgImpl.u and ArgImpl2.u *) +Check FnApp2.bar. + +(** It can be shadowed *) +Universe u. + +(** This refers to the qualified name *) +Check FnApp2.bar. + +Constraint u = ArgImpl.u. +Print Universes. + +Set Universe Polymorphism. + +Section PS. + Universe poly. + + Definition id (A : Type@{poly}) (a : A) : A := a. +End PS. +(** The universe is polymorphic and discharged, does not persist *) +Fail Check Type@{poly}. + +Print Universes. +Check id nat. +Check id@{Set}. |