diff options
Diffstat (limited to 'test-suite')
65 files changed, 492 insertions, 118 deletions
diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v new file mode 100644 index 0000000000..6ff394bca6 --- /dev/null +++ b/test-suite/bugs/closed/bug_3468.v @@ -0,0 +1,29 @@ +(* Checking that unrelated terms requiring some scope do not affect + the interpretation of tactic-in-term. The "Check" was failing with: + The term "Set" has type "Type" while it is expected to have type + "nat". *) + +Notation bar2 a b := (let __ := ltac:(exact I) in (a + b)%type) (only parsing). +Check bar2 (Set + Set) Set. + +(* Taking into account scopes in notations containing tactic-in-term *) + +Declare Scope foo_scope. +Delimit Scope foo_scope with foo. +Notation "x ~~" := (x) (at level 0, only parsing) : foo_scope. +Notation bar x := (x%foo) (only parsing). +Notation baz x := ltac:(exact x%foo) (only parsing). +Check bar (O ~~). +Check baz (O ~~). (* Was failing *) + +(* This was reported as bug #8706 *) + +Declare Scope my_scope. +Notation "@ a" := a%nat (at level 100, only parsing) : my_scope. +Delimit Scope my_scope with my. + +Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope. +Definition test := (& (@4))%my. + +(* Check inconsistent scopes *) +Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing). diff --git a/test-suite/bugs/closed/bug_8544.v b/test-suite/bugs/closed/bug_8544.v new file mode 100644 index 0000000000..674d112595 --- /dev/null +++ b/test-suite/bugs/closed/bug_8544.v @@ -0,0 +1,6 @@ +Require Import ssreflect. +Goal True \/ True -> False. +Proof. +(* the following should fail: 2 subgoals, but only one intro pattern *) +Fail case => [a]. +Abort. diff --git a/test-suite/bugs/closed/bug_8755.v b/test-suite/bugs/closed/bug_8755.v new file mode 100644 index 0000000000..cd5aee4fa0 --- /dev/null +++ b/test-suite/bugs/closed/bug_8755.v @@ -0,0 +1,6 @@ + +Lemma f : Type. +Fail let i := ident:(i) in +let t := context i [Type] in +idtac. +Abort. diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v new file mode 100644 index 0000000000..b10569499e --- /dev/null +++ b/test-suite/bugs/closed/bug_8785.v @@ -0,0 +1,44 @@ +Universe u v w. +Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := . + +Inductive FiniteT : Type -> Prop := + | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T) + | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X -> + invertible f -> FiniteT Y. + +Set Printing Universes. + +Axiom a : False. +(* +Constraint v <= u. +Constraint v <= w. +*) +Lemma finite_subtype: forall (X:Type) (P:X->Prop), + FiniteT X -> (forall x:X, P x \/ ~ P x) -> + FiniteT {x:X | P x}. +Proof. +intros. +induction H. + +destruct (H0 None). +elim a. + +pose (g := fun (x:{x:T | P (Some x)}) => + match x return {x:option T | P x} with + | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +pose (g := fun (x:{x:X | P (f x)}) => + match x with + | exist _ x0 i => exist (fun x:Y => P x) (f x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +Qed. diff --git a/test-suite/bugs/closed/bug_8791.v b/test-suite/bugs/closed/bug_8791.v new file mode 100644 index 0000000000..9be1936cdf --- /dev/null +++ b/test-suite/bugs/closed/bug_8791.v @@ -0,0 +1,9 @@ +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. + +Definition A := 42. + +Instance foo (A: Type): Inhabited (list A). +Check A. +Abort. + +Fail Instance foo (A : nat) (A : Type) : Inhabited nat. diff --git a/test-suite/bugs/closed/bug_8794.v b/test-suite/bugs/closed/bug_8794.v new file mode 100644 index 0000000000..5ff0b30260 --- /dev/null +++ b/test-suite/bugs/closed/bug_8794.v @@ -0,0 +1,11 @@ +(* This used to raise an anomaly in 8.8 *) + +Inductive T := Tau (t : T). + +Notation idT t := (match t with Tau t => Tau t end). + +Lemma match_itree : forall (t : T), t = idT t. +Proof. destruct t; auto. Qed. + +Lemma what (k : unit -> T) : k tt = k tt. +Proof. rewrite match_itree. Abort. diff --git a/test-suite/bugs/closed/bug_8848.v b/test-suite/bugs/closed/bug_8848.v new file mode 100644 index 0000000000..26563e6747 --- /dev/null +++ b/test-suite/bugs/closed/bug_8848.v @@ -0,0 +1,18 @@ +Require Import Program. +Set Implicit Arguments. +Unset Strict Implicit. + +Definition def (a : nat) := a = a. + +Structure record {a : nat} {D : def a} := + inR { prop : Prop }. + +Program +Canonical Structure ins (a : nat) (rec : @record a _) := + @inR a _ (prop rec). +Next Obligation. + exact eq_refl. +Defined. +Next Obligation. + exact eq_refl. +Defined. diff --git a/test-suite/coq-makefile/arg/_CoqProject b/test-suite/coq-makefile/arg/_CoqProject index 53dc963997..ed31a58247 100644 --- a/test-suite/coq-makefile/arg/_CoqProject +++ b/test-suite/coq-makefile/arg/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/compat-subdirs/_CoqProject b/test-suite/coq-makefile/compat-subdirs/_CoqProject index 4f44bde22a..1f914a71b0 100644 --- a/test-suite/coq-makefile/compat-subdirs/_CoqProject +++ b/test-suite/coq-makefile/compat-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc1/_CoqProject b/test-suite/coq-makefile/coqdoc1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/coqdoc1/_CoqProject +++ b/test-suite/coq-makefile/coqdoc1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/coqdoc2/_CoqProject b/test-suite/coq-makefile/coqdoc2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/coqdoc2/_CoqProject +++ b/test-suite/coq-makefile/coqdoc2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/emptyprefix/_CoqProject b/test-suite/coq-makefile/emptyprefix/_CoqProject index 5678a8edbb..3133342f6c 100644 --- a/test-suite/coq-makefile/emptyprefix/_CoqProject +++ b/test-suite/coq-makefile/emptyprefix/_CoqProject @@ -4,7 +4,7 @@ -arg "-w default" src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/extend-subdirs/_CoqProject b/test-suite/coq-makefile/extend-subdirs/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/extend-subdirs/_CoqProject +++ b/test-suite/coq-makefile/extend-subdirs/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/findlib-package/_CoqProject b/test-suite/coq-makefile/findlib-package/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/findlib-package/_CoqProject +++ b/test-suite/coq-makefile/findlib-package/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/latex1/_CoqProject b/test-suite/coq-makefile/latex1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/latex1/_CoqProject +++ b/test-suite/coq-makefile/latex1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/merlin1/_CoqProject b/test-suite/coq-makefile/merlin1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/merlin1/_CoqProject +++ b/test-suite/coq-makefile/merlin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack1/_CoqProject b/test-suite/coq-makefile/mlpack1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/mlpack1/_CoqProject +++ b/test-suite/coq-makefile/mlpack1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/mlpack2/_CoqProject b/test-suite/coq-makefile/mlpack2/_CoqProject index 51864a87ae..3db54e0a0b 100644 --- a/test-suite/coq-makefile/mlpack2/_CoqProject +++ b/test-suite/coq-makefile/mlpack2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/multiroot/_CoqProject b/test-suite/coq-makefile/multiroot/_CoqProject index b384bb6d97..f53eef99a8 100644 --- a/test-suite/coq-makefile/multiroot/_CoqProject +++ b/test-suite/coq-makefile/multiroot/_CoqProject @@ -4,7 +4,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/native1/_CoqProject b/test-suite/coq-makefile/native1/_CoqProject index a6fa17348c..3dfca7ffc0 100644 --- a/test-suite/coq-makefile/native1/_CoqProject +++ b/test-suite/coq-makefile/native1/_CoqProject @@ -2,9 +2,10 @@ -R theories test -I src -arg -native-compiler +-arg yes src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/only/_CoqProject b/test-suite/coq-makefile/only/_CoqProject index 357384fddf..619a8fa459 100644 --- a/test-suite/coq-makefile/only/_CoqProject +++ b/test-suite/coq-makefile/only/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mlpack -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin1/_CoqProject b/test-suite/coq-makefile/plugin1/_CoqProject index 4eddc9d708..ab7876d868 100644 --- a/test-suite/coq-makefile/plugin1/_CoqProject +++ b/test-suite/coq-makefile/plugin1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin2/_CoqProject b/test-suite/coq-makefile/plugin2/_CoqProject index 0bf1e07f25..94eed53130 100644 --- a/test-suite/coq-makefile/plugin2/_CoqProject +++ b/test-suite/coq-makefile/plugin2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mllib -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/plugin3/_CoqProject b/test-suite/coq-makefile/plugin3/_CoqProject index 2028d49a8b..8e8a7ab074 100644 --- a/test-suite/coq-makefile/plugin3/_CoqProject +++ b/test-suite/coq-makefile/plugin3/_CoqProject @@ -3,7 +3,7 @@ -I src/ ./src/test_plugin.mllib -./src/test.ml4 +./src/test.mlg ./src/test.mli ./src/test_aux.ml ./src/test_aux.mli diff --git a/test-suite/coq-makefile/quick2vo/_CoqProject b/test-suite/coq-makefile/quick2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/quick2vo/_CoqProject +++ b/test-suite/coq-makefile/quick2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/template/init.sh b/test-suite/coq-makefile/template/init.sh index 2e066d30d9..30be5e6456 100755 --- a/test-suite/coq-makefile/template/init.sh +++ b/test-suite/coq-makefile/template/init.sh @@ -11,7 +11,7 @@ mkdir -p theories/sub cp ../../template/theories/sub/testsub.v theories/sub cp ../../template/theories/test.v theories -cp ../../template/src/test.ml4 src +cp ../../template/src/test.mlg src cp ../../template/src/test_aux.mli src cp ../../template/src/test.mli src cp ../../template/src/test_plugin.mlpack src diff --git a/test-suite/coq-makefile/template/src/test.ml4 b/test-suite/coq-makefile/template/src/test.mlg index 72765abe04..7a166f3b98 100644 --- a/test-suite/coq-makefile/template/src/test.ml4 +++ b/test-suite/coq-makefile/template/src/test.mlg @@ -1,13 +1,17 @@ +{ open Ltac_plugin +} DECLARE PLUGIN "test_plugin" +{ let () = Mltop.add_known_plugin (fun () -> ()) "test_plugin";; +} VERNAC COMMAND EXTEND Test CLASSIFIED AS SIDEFF - | [ "TestCommand" ] -> [ () ] + | [ "TestCommand" ] -> { () } END TACTIC EXTEND test -| [ "test_tactic" ] -> [ Test_aux.tac ] +| [ "test_tactic" ] -> { Test_aux.tac } END diff --git a/test-suite/coq-makefile/uninstall1/_CoqProject b/test-suite/coq-makefile/uninstall1/_CoqProject index 35792066bb..aa9473eaf0 100644 --- a/test-suite/coq-makefile/uninstall1/_CoqProject +++ b/test-suite/coq-makefile/uninstall1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/uninstall2/_CoqProject b/test-suite/coq-makefile/uninstall2/_CoqProject index d2a547d47b..0068554d72 100644 --- a/test-suite/coq-makefile/uninstall2/_CoqProject +++ b/test-suite/coq-makefile/uninstall2/_CoqProject @@ -3,7 +3,7 @@ -I src/ src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/validate1/_CoqProject b/test-suite/coq-makefile/validate1/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/validate1/_CoqProject +++ b/test-suite/coq-makefile/validate1/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coq-makefile/vio2vo/_CoqProject b/test-suite/coq-makefile/vio2vo/_CoqProject index 69f47302e1..61136e82f0 100644 --- a/test-suite/coq-makefile/vio2vo/_CoqProject +++ b/test-suite/coq-makefile/vio2vo/_CoqProject @@ -3,7 +3,7 @@ -I src src/test_plugin.mlpack -src/test.ml4 +src/test.mlg src/test.mli src/test_aux.ml src/test_aux.mli diff --git a/test-suite/coqchk/bug_8655.v b/test-suite/coqchk/bug_8655.v new file mode 100644 index 0000000000..06d08b2082 --- /dev/null +++ b/test-suite/coqchk/bug_8655.v @@ -0,0 +1 @@ +Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). diff --git a/test-suite/coqchk/bug_8876.v b/test-suite/coqchk/bug_8876.v new file mode 100644 index 0000000000..2d20511a04 --- /dev/null +++ b/test-suite/coqchk/bug_8876.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) +Require Import Coq.Init.Notations. + +Notation "x -> y" := (forall _ : x, y). + +Inductive eq {A:Type} (a:A) : A -> Prop := eq_refl : eq a a. + +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. +Set Printing Universes. + +(* Constructors for an inductive with indices *) +Module WithIndex. + Inductive foo@{i} : (Prop -> Prop) -> Prop := mkfoo: foo (fun x => x). + + Monomorphic Universes i j. + Monomorphic Constraint i < j. + Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _. +End WithIndex. diff --git a/test-suite/coqchk/bug_8881.v b/test-suite/coqchk/bug_8881.v new file mode 100644 index 0000000000..dfc209b318 --- /dev/null +++ b/test-suite/coqchk/bug_8881.v @@ -0,0 +1,23 @@ + +(* Check use of equivalence on inductive types (bug #1242) *) + +Module Type ASIG. + Inductive t : Set := a | b : t. + Definition f := fun x => match x with a => true | b => false end. +End ASIG. + +Module Type BSIG. + Declare Module A : ASIG. + Definition f := fun x => match x with A.a => true | A.b => false end. +End BSIG. + +Module C (A : ASIG) (B : BSIG with Module A:=A). + + (* Check equivalence is considered in "case_info" *) + Lemma test : forall x, A.f x = B.f x. + Proof. + intro x. unfold B.f, A.f. + destruct x; reflexivity. + Qed. + +End C. diff --git a/test-suite/misc/poly-capture-global-univs/.gitignore b/test-suite/misc/poly-capture-global-univs/.gitignore index f5a6d22b8e..2a6a6bc68d 100644 --- a/test-suite/misc/poly-capture-global-univs/.gitignore +++ b/test-suite/misc/poly-capture-global-univs/.gitignore @@ -1 +1,2 @@ /Makefile* +/src/evil.ml diff --git a/test-suite/misc/poly-capture-global-univs/_CoqProject b/test-suite/misc/poly-capture-global-univs/_CoqProject index 70ec246062..e5dc3cff56 100644 --- a/test-suite/misc/poly-capture-global-univs/_CoqProject +++ b/test-suite/misc/poly-capture-global-univs/_CoqProject @@ -1,7 +1,7 @@ -Q theories Evil -I src -src/evil.ml4 +src/evil.mlg src/evilImpl.ml src/evilImpl.mli src/evil_plugin.mlpack diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 b/test-suite/misc/poly-capture-global-univs/src/evil.ml4 deleted file mode 100644 index 565e979aaa..0000000000 --- a/test-suite/misc/poly-capture-global-univs/src/evil.ml4 +++ /dev/null @@ -1,9 +0,0 @@ - -open Stdarg -open EvilImpl - -DECLARE PLUGIN "evil_plugin" - -VERNAC COMMAND FUNCTIONAL EXTEND VernacEvil CLASSIFIED AS SIDEFF -| [ "Evil" ident(x) ident(y) ] -> [ fun ~atts ~st -> evil x y; st ] -END diff --git a/test-suite/misc/poly-capture-global-univs/src/evil.mlg b/test-suite/misc/poly-capture-global-univs/src/evil.mlg new file mode 100644 index 0000000000..edd22b1d29 --- /dev/null +++ b/test-suite/misc/poly-capture-global-univs/src/evil.mlg @@ -0,0 +1,10 @@ +{ +open Stdarg +open EvilImpl +} + +DECLARE PLUGIN "evil_plugin" + +VERNAC COMMAND EXTEND VernacEvil CLASSIFIED AS SIDEFF +| [ "Evil" ident(x) ident(y) ] -> { evil x y } +END diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index 6d8ce7c5d7..047f4cd080 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -15,7 +15,7 @@ let evil t f = let tc = mkConst tc in let fe = Declare.definition_entry - ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty))) + ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) ~types:(Term.mkArrow tc tu) (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1)) in diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index d587d1f09b..7074ad2d41 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,11 +1,13 @@ Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when applied to 1 argument but avoid exposing match constructs @@ -13,6 +15,7 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and @@ -21,6 +24,7 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments @@ -28,6 +32,7 @@ Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat +Nat.sub is not universe polymorphic Argument scopes are [nat_scope nat_scope] The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor @@ -37,6 +42,7 @@ pf : forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 +pf is not universe polymorphic Arguments D2, C2 are implicit Arguments D1, C1 are implicit and maximally inserted Argument scopes are [foo_scope type_scope _ _ _ _ _] @@ -45,6 +51,7 @@ pf is transparent Expands to: Constant Arguments.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C +fcomp is not universe polymorphic Arguments A, B, C are implicit and maximally inserted Argument scopes are [type_scope type_scope type_scope _ _ _] The reduction tactics unfold fcomp when applied to 6 arguments @@ -52,17 +59,20 @@ fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat +volatile is not universe polymorphic Argument scope is [nat_scope] The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Arguments.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] f is transparent Expands to: Constant Arguments.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument scopes are [_ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor @@ -70,6 +80,7 @@ f is transparent Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Argument T2 is implicit Argument scopes are [type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 4th, 5th and @@ -78,6 +89,7 @@ f is transparent Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic Arguments T1, T2 are implicit Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] The reduction tactics unfold f when the 5th, 6th and @@ -90,6 +102,7 @@ Expands to: Constant Arguments.f : Prop f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat +f is not universe polymorphic The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index febe160820..69ba329ff1 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,56 +1,70 @@ a : bool -> bool +a is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable a b : bool -> bool +b is not universe polymorphic Argument scope is [bool_scope] Expands to: Variable b negb'' : bool -> bool +negb'' is not universe polymorphic Argument scope is [bool_scope] negb'' is transparent Expands to: Constant ArgumentsScope.A.B.negb'' negb' : bool -> bool +negb' is not universe polymorphic Argument scope is [bool_scope] negb' is transparent Expands to: Constant ArgumentsScope.A.negb' negb : bool -> bool +negb is not universe polymorphic Argument scope is [bool_scope] negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool +a is not universe polymorphic Expands to: Variable a b : bool -> bool +b is not universe polymorphic Expands to: Variable b negb : bool -> bool +negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool +negb' is not universe polymorphic negb' is transparent Expands to: Constant ArgumentsScope.A.negb' negb'' : bool -> bool +negb'' is not universe polymorphic negb'' is transparent Expands to: Constant ArgumentsScope.A.B.negb'' a : bool -> bool +a is not universe polymorphic Expands to: Variable a negb : bool -> bool +negb is not universe polymorphic negb is transparent Expands to: Constant Coq.Init.Datatypes.negb negb' : bool -> bool +negb' is not universe polymorphic negb' is transparent Expands to: Constant ArgumentsScope.negb' negb'' : bool -> bool +negb'' is not universe polymorphic negb'' is transparent Expands to: Constant ArgumentsScope.negb'' diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 1755886967..b071da86c9 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ eq_refl : ?y = ?y where ?y : [ |- nat] -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y For eq: Argument A is implicit and maximally inserted @@ -23,6 +23,7 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x +eq_refl is not universe polymorphic Arguments are renamed to B, y When applied to no arguments: Arguments B, y are implicit and maximally inserted @@ -30,7 +31,8 @@ When applied to 1 argument: Argument B is implicit Argument scopes are [type_scope _] Expands to: Constructor Coq.Init.Logic.eq_refl -Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x +Monomorphic Inductive myEq (B : Type) (x : A) : A -> Prop := + myrefl : B -> myEq B x x For myrefl: Arguments are renamed to C, x, _ For myrefl: Argument C is implicit and maximally inserted @@ -38,11 +40,12 @@ For myEq: Argument scopes are [type_scope _ _] For myrefl: Argument scopes are [type_scope _ _] myrefl : forall (B : Type) (x : A), B -> myEq B x x +myrefl is not universe polymorphic Arguments are renamed to C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope _ _] Expands to: Constructor Arguments_renaming.Test1.myrefl -myplus = +Monomorphic myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with | 0 => m @@ -50,11 +53,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] @@ -64,7 +69,7 @@ myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat -Inductive myEq (A B : Type) (x : A) : A -> Prop := +Monomorphic Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x For myrefl: Arguments are renamed to A, C, x, _ @@ -73,13 +78,14 @@ For myEq: Argument scopes are [type_scope type_scope _ _] For myrefl: Argument scopes are [type_scope type_scope _ _] myrefl : forall (A B : Type) (x : A), B -> myEq A B x x +myrefl is not universe polymorphic Arguments are renamed to A, C, x, _ Argument C is implicit and maximally inserted Argument scopes are [type_scope type_scope _ _] Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x -myplus = +Monomorphic myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := match n with | 0 => m @@ -87,11 +93,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] myplus : forall T : Type, T -> nat -> nat -> nat +myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out index 34558e9a6b..9c46ace463 100644 --- a/test-suite/output/Binder.out +++ b/test-suite/output/Binder.out @@ -1,8 +1,12 @@ -foo = fun '(x, y) => x + y +Monomorphic foo = fun '(x, y) => x + y : nat * nat -> nat + +foo is not universe polymorphic forall '(a, b), a /\ b : Prop -foo = λ '(x, y), x + y +Monomorphic foo = λ '(x, y), x + y : nat * nat → nat + +foo is not universe polymorphic ∀ '(a, b), a ∧ b : Prop diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index cb835ab48d..0a02c5a7dd 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -1,4 +1,4 @@ -t_rect = +Monomorphic t_rect = fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) => fix F (t : t) : P t := match t as t0 return (P t0) with @@ -7,6 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t +t_rect is not universe polymorphic Argument scopes are [function_scope function_scope _] = fun d : TT => match d with | {| f3 := b |} => b @@ -16,7 +17,7 @@ Argument scopes are [function_scope function_scope _] | {| f3 := b |} => b end : TT -> 0 = 0 -proj = +Monomorphic proj = fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) => match Nat.eq_dec x y with | left eqprf => match eqprf in (_ = z) return (P z) with @@ -26,8 +27,9 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y +proj is not universe polymorphic Argument scopes are [nat_scope nat_scope function_scope _ _] -foo = +Monomorphic foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with | nil => None @@ -36,17 +38,21 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A +foo is not universe polymorphic Argument scopes are [type_scope list_scope] -uncast = +Monomorphic uncast = fun (A : Type) (x : I A) => match x with | x0 <: _ => x0 end : forall A : Type, I A -> A +uncast is not universe polymorphic Argument scopes are [type_scope _] -foo' = if A 0 then true else false +Monomorphic foo' = if A 0 then true else false : bool -f = + +foo' is not universe polymorphic +Monomorphic f = fun H : B => match H with | AC x => @@ -56,6 +62,8 @@ match H with else fun _ : P false => Logic.I) x end : B -> True + +f is not universe polymorphic The command has indeed failed with message: Non exhaustive pattern-matching: no clause found for pattern gadtTy _ _ @@ -75,17 +83,22 @@ fun '(D n m p q) => n + m + p + q : J -> nat The command has indeed failed with message: The constructor D (in type J) expects 3 arguments. -lem1 = +Monomorphic lem1 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k -lem2 = + +lem1 is not universe polymorphic +Monomorphic lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k +lem2 is not universe polymorphic Argument scope is [bool_scope] -lem3 = +Monomorphic lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k + +lem3 is not universe polymorphic 1 subgoal x : nat diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 3b65003c29..71c7070f2b 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -2,9 +2,11 @@ compose (C:=nat) S : (nat -> nat) -> nat -> nat ex_intro (P:=fun _ : nat => True) (x:=0) I : ex (fun _ : nat => True) -d2 = fun x : nat => d1 (y:=x) +Monomorphic d2 = +fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x +d2 is not universe polymorphic Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] map id (1 :: nil) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index af202ea01c..6d65db9e22 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,7 +1,8 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". -Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x +Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop := + Foo : foo A x For foo: Argument scopes are [type_scope _] For Foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index c17c63e724..4743fb0d0a 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,4 +1,4 @@ -Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := +Monomorphic Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} For sig2: Argument A is implicit diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out index 0904d5540b..f84cedfa62 100644 --- a/test-suite/output/Load.out +++ b/test-suite/output/Load.out @@ -1,6 +1,10 @@ -f = 2 +Monomorphic f = 2 : nat -u = I + +f is not universe polymorphic +Monomorphic u = I : True + +u is not universe polymorphic The command has indeed failed with message: Files processed by Load cannot leave open proofs. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index d32cf67e28..48379f713d 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -223,13 +223,14 @@ fun S : nat => [[S | S.S]] : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop -foo = +Monomorphic foo = fun l : list nat => match l with | _ :: (_ :: _) as l1 => l1 | _ => l end : list nat -> list nat +foo is not universe polymorphic Argument scope is [list_scope] Notation "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index cef7d1a702..46784d1897 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,7 @@ [< 0 > + < 1 > * < 2 >] : nat +[< b > + < b > * < 2 >] + : nat [<< # 0 >>] : option nat [1 {f 1}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 9738ce5a5e..6bdbf1bed5 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Axiom a : nat. +Notation b := a. +Check [ < b > + < a > * < 2 >]. + Declare Custom Entry anotherconstr. Notation "[ x ]" := x (x custom myconstr at level 6). diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 8a6d94c732..bfeff20524 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -1,20 +1,31 @@ -swap = fun '(x, y) => (y, x) +Monomorphic swap = fun '(x, y) => (y, x) : A * B -> B * A + +swap is not universe polymorphic fun '(x, y) => (y, x) : A * B -> B * A forall '(x, y), swap (x, y) = (y, x) : Prop -proj_informative = fun '(exist _ x _) => x : A +Monomorphic proj_informative = +fun '(exist _ x _) => x : A : {x : A | P x} -> A -foo = fun '(Bar n b tt p) => if b then n + p else n - p + +proj_informative is not universe polymorphic +Monomorphic foo = +fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat -baz = + +foo is not universe polymorphic +Monomorphic baz = fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1 : Foo -> Foo -> nat -swap = + +baz is not universe polymorphic +Monomorphic swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A +swap is not universe polymorphic Arguments A, B are implicit and maximally inserted Argument scopes are [type_scope type_scope _] fun (A B : Type) '(x, y) => swap (x, y) = (y, x) @@ -29,19 +40,22 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w) : A * B → B * A ∀ '(x, y), swap (x, y) = (y, x) : Prop -both_z = +Monomorphic both_z = fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat + +both_z is not universe polymorphic fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop fun (pat : nat) '(x, y) => x + y = pat : nat -> nat * nat -> Prop -f = fun x : nat => x + x +Monomorphic f = fun x : nat => x + x : nat -> nat +f is not universe polymorphic Argument scope is [nat_scope] fun x : nat => x + x : nat -> nat diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 38a16e01c2..be793dd453 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -4,7 +4,7 @@ existT is template universe polymorphic Argument A is implicit Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT -Inductive sigT (A : Type) (P : A -> Type) : Type := +Monomorphic Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} For sigT: Argument A is implicit @@ -14,7 +14,7 @@ For existT: Argument scopes are [type_scope function_scope _ _] existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: @@ -25,6 +25,7 @@ For eq: Argument scopes are [type_scope _ _] For eq_refl: Argument scopes are [type_scope _] eq_refl : forall (A : Type) (x : A), x = x +eq_refl is not universe polymorphic When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: @@ -37,7 +38,7 @@ When applied to no arguments: Arguments A, x are implicit and maximally inserted When applied to 1 argument: Argument A is implicit -Nat.add = +Monomorphic Nat.add = fix add (n m : nat) {struct n} : nat := match n with | 0 => m @@ -45,9 +46,11 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat +Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] Nat.add : nat -> nat -> nat +Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] Nat.add is transparent Expands to: Constant Coq.Init.Nat.add @@ -55,10 +58,11 @@ Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 +plus_n_O is not universe polymorphic Argument scope is [nat_scope] plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O -Inductive le (n : nat) : nat -> Prop := +Monomorphic Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m For le_S: Argument m is implicit @@ -68,18 +72,21 @@ For le_n: Argument scope is [nat_scope] For le_S: Argument scopes are [nat_scope nat_scope _] comparison : Set +comparison is not universe polymorphic Expands to: Inductive Coq.Init.Datatypes.comparison -Inductive comparison : Set := +Monomorphic Inductive comparison : Set := Eq : comparison | Lt : comparison | Gt : comparison bar : foo +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 Argument x is implicit and maximally inserted Expands to: Constant PrintInfos.bar -*** [ bar : foo ] +Monomorphic *** [ bar : foo ] +bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 @@ -87,7 +94,7 @@ Argument x is implicit and maximally inserted Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq -Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x +Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq: Argument A is implicit and maximally inserted For eq_refl, when applied to no arguments: diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out new file mode 100644 index 0000000000..5b67f632c9 --- /dev/null +++ b/test-suite/output/RecordFieldErrors.out @@ -0,0 +1,14 @@ +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record contains fields of both t and t'. +The command has indeed failed with message: +unit: Not a projection. +The command has indeed failed with message: +This record defines several times the field foo. +The command has indeed failed with message: +This record defines several times the field unit. +The command has indeed failed with message: +unit: Not a projection of inductive t. diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v new file mode 100644 index 0000000000..27aa07822b --- /dev/null +++ b/test-suite/output/RecordFieldErrors.v @@ -0,0 +1,38 @@ +(** Check that various errors in record fields are reported with the correct +underlying issue. *) + +Record t := + { foo: unit }. + +Record t' := + { bar: unit }. + +Fail Check {| unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| unit := tt; + foo := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + bar := tt |}. +(* This record contains fields of both t and t'. *) + +Fail Check {| unit := tt; + unit := tt |}. +(* unit: Not a projection. *) + +Fail Check {| foo := tt; + foo := tt |}. +(* This record defines several times the field foo. *) + +Fail Check {| foo := tt; + unit := tt; + unit := tt |}. +(* This is slightly wrong (would prefer "unit: Not a projection."), but it's +acceptable and seems an unlikely mistake. *) +(* This record defines several times the field unit. *) + +Fail Check {| foo := tt; + unit := tt |}. +(* unit: Not a projection of inductive t. *) diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index f94ed64234..f080f6d0f0 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,7 +1,15 @@ -TrM.A = M.A +Monomorphic TrM.A = M.A : Set -OpM.A = M.A + +TrM.A is not universe polymorphic +Monomorphic OpM.A = M.A : Set -TrM.B = M.B + +OpM.A is not universe polymorphic +Monomorphic TrM.B = M.B : Set -*** [ OpM.B : Set ] + +TrM.B is not universe polymorphic +Monomorphic *** [ OpM.B : Set ] + +OpM.B is not universe polymorphic diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index acc37f653c..178116c580 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -1,34 +1,37 @@ -NonCumulative Inductive Empty@{u} : Type@{u} := -NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } +Polymorphic NonCumulative Inductive Empty@{u} : Type@{u} := +Polymorphic 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} = +Polymorphic 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 } +Polymorphic 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} = +Polymorphic 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 +Polymorphic Wrap@{u} = +fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) Wrap is universe polymorphic Argument scope is [type_scope] -wrap@{u} = +Polymorphic wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) @@ -36,13 +39,13 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap wrap is universe polymorphic Arguments A, Wrap are implicit and maximally inserted Argument scopes are [type_scope _] -bar@{u} = nat +Polymorphic bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) bar is universe polymorphic -foo@{u UnivBinders.17 v} = +Polymorphic foo@{u UnivBinders.17 v} = Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) @@ -75,25 +78,28 @@ mono : Type@{mono.u+1} The command has indeed failed with message: Universe u already exists. -bobmorane = +Monomorphic bobmorane = let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff : Type@{max(tt.u,ff.u)} + +bobmorane is not universe polymorphic The command has indeed failed with message: Universe u already bound. -foo@{E M N} = +Polymorphic 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@{u UnivBinders.17 v} = +Polymorphic foo@{u UnivBinders.17 v} = Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) foo is universe polymorphic -NonCumulative Inductive Empty@{E} : Type@{E} := -NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } +Polymorphic NonCumulative Inductive Empty@{E} : Type@{E} := +Polymorphic 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] @@ -119,70 +125,77 @@ Type@{bind_univs.mono.u} (* {bind_univs.mono.u} |= *) bind_univs.mono is not universe polymorphic -bind_univs.poly@{u} = Type@{u} +Polymorphic bind_univs.poly@{u} = Type@{u} : Type@{u+1} (* u |= *) bind_univs.poly is universe polymorphic -insec@{v} = Type@{u} -> Type@{v} +Polymorphic insec@{v} = +Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) insec is universe polymorphic -NonCumulative Inductive insecind@{k} : Type@{k+1} := +Polymorphic NonCumulative Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} For inseccstr: Argument scope is [type_scope] -insec@{u v} = Type@{u} -> Type@{v} +Polymorphic insec@{u v} = +Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic -NonCumulative Inductive insecind@{u k} : Type@{k+1} := +Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} For inseccstr: Argument scope is [type_scope] -inmod@{u} = Type@{u} +Polymorphic insec2@{u} = Prop + : Type@{Set+1} +(* u |= *) + +insec2 is universe polymorphic +Polymorphic inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) inmod is universe polymorphic -SomeMod.inmod@{u} = Type@{u} +Polymorphic SomeMod.inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) SomeMod.inmod is universe polymorphic -inmod@{u} = Type@{u} +Polymorphic inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) inmod is universe polymorphic -Applied.infunct@{u v} = +Polymorphic Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i UnivBinders.55 UnivBinders.56} : -Type@{UnivBinders.55} -> Type@{i} -(* i UnivBinders.55 UnivBinders.56 |= *) +axfoo@{i UnivBinders.56 UnivBinders.57} : +Type@{UnivBinders.56} -> Type@{i} +(* i UnivBinders.56 UnivBinders.57 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.55 UnivBinders.56} : -Type@{UnivBinders.56} -> Type@{i} -(* i UnivBinders.55 UnivBinders.56 |= *) +axbar@{i UnivBinders.56 UnivBinders.57} : +Type@{UnivBinders.57} -> Type@{i} +(* i UnivBinders.56 UnivBinders.57 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axbar -axfoo' : Type@{UnivBinders.58} -> Type@{axbar'.i} +axfoo' : Type@{UnivBinders.59} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo' -axbar' : Type@{UnivBinders.58} -> Type@{axbar'.i} +axbar' : Type@{UnivBinders.59} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 56474a0723..19d241d35d 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -130,6 +130,12 @@ End SomeSec. Print insec. Print insecind. +Section SomeSec2. + Universe u. + Definition insec2@{} := Prop. +End SomeSec2. +Print insec2. + Module SomeMod. Definition inmod@{u} := Type@{u}. Print inmod. diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 773533a8d3..3dad2360c4 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -1,7 +1,11 @@ -Nat.t = nat +Monomorphic Nat.t = nat : Set -Nat.t = nat + +Nat.t is not universe polymorphic +Monomorphic Nat.t = nat : Set + +Nat.t is not universe polymorphic 1 subgoal ============================ diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index f7ffd1959a..a1326596bb 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -1,9 +1,11 @@ -P = +Monomorphic P = fun e : option L => match e with | Some cl => Some cl | None => None end : option L -> option L + +P is not universe polymorphic fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index ebf5b094e1..2f13b7c225 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -169,7 +169,7 @@ Proof. Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. -Timeout 1 Fail apply _. (* 0.06s *) + Timeout 1 Fail apply _. (* 0.06s *) Abort. End HintCut. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index f07c0191f1..c2130995fc 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -1,7 +1,5 @@ (* Test des definitions inductives imbriquees *) -Require Import List. - Inductive X : Set := cons1 : list X -> X. diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v index 1c6e2d81d8..cfc25c3346 100644 --- a/test-suite/success/Template.v +++ b/test-suite/success/Template.v @@ -25,7 +25,7 @@ Module AutoNo. End AutoNo. Module Yes. - #[template] + #[universes(template)] Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A. About Box. @@ -37,7 +37,7 @@ Module Yes. End Yes. Module No. - #[notemplate] + #[universes(notemplate)] Inductive Box (A:Type) : Type := box : A -> Box A. About Box. diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index 7b972f4ed9..f4f59a3c16 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -11,7 +11,7 @@ End Scope. Fail Check 0 = true :> nat. -#[polymorphic] +#[universes(polymorphic)] Definition ι T (x: T) := x. Check ι _ ι. @@ -24,9 +24,9 @@ Reset f. Ltac foo := foo. Module M. - #[local] #[polymorphic] Definition zed := Type. + #[local] #[universes(polymorphic)] Definition zed := Type. - #[local, polymorphic] Definition kats := Type. + #[local, universes(polymorphic)] Definition kats := Type. End M. Check M.zed@{_}. Fail Check zed. diff --git a/test-suite/success/module_with_def_univ_poly.v b/test-suite/success/module_with_def_univ_poly.v new file mode 100644 index 0000000000..a547be4c46 --- /dev/null +++ b/test-suite/success/module_with_def_univ_poly.v @@ -0,0 +1,31 @@ + +(* When doing Module Foo with Definition bar := ..., bar must be + generated with the same polymorphism as Foo.bar. *) +Module Mono. + Unset Universe Polymorphism. + Module Type T. + Parameter foo : Type. + End T. + + Module Type F(A:T). End F. + + Set Universe Polymorphism. + Module M : T with Definition foo := Type. + Monomorphic Definition foo := Type. + End M. +End Mono. + +Module Poly. + Set Universe Polymorphism. + + Module Type T. + Parameter foo@{i|Set < i} : Type@{i}. + End T. + + Module Type F(A:T). End F. + + Unset Universe Polymorphism. + Module M : T with Definition foo := Set : Type. + Polymorphic Definition foo := Set : Type. + End M. +End Poly. |