From 6a046f8d3e33701d70e2a391741e65564cc0554d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 23 Jan 2016 15:55:43 -0500 Subject: Fix bug #4519: oops, global shadowed local universe level bindings. --- test-suite/bugs/closed/4519.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 test-suite/bugs/closed/4519.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v new file mode 100644 index 0000000000..ccbc47d20f --- /dev/null +++ b/test-suite/bugs/closed/4519.v @@ -0,0 +1,21 @@ +Set Universe Polymorphism. +Section foo. + Universe i. + Context (foo : Type@{i}) (bar : Type@{i}). + Definition qux@{i} (baz : Type@{i}) := foo -> bar. +End foo. +Set Printing Universes. +Print qux. (* qux@{Top.42 Top.43} = +fun foo bar _ : Type@{Top.42} => foo -> bar + : Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} +(* Top.42 Top.43 |= *) +(* This is wrong; the first two types are equal, but the last one is not *) + +qux is universe polymorphic +Argument scopes are [type_scope type_scope type_scope] + *) +Check qux nat nat nat : Set. +Check qux nat nat Set : Set. (* Error: +The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is +expected to have type "Set" +(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *) \ No newline at end of file -- cgit v1.2.3 From b582db2ecbb3f7f1315fedc50b0009f62f5c59ad Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 23 Jan 2016 17:28:34 -0500 Subject: Fix bug #4503: mixing universe polymorphic and monomorphic variables and definitions in sections is unsupported. --- test-suite/bugs/closed/4503.v | 37 +++++++++++++++++++++++++++++++++++ test-suite/bugs/closed/HoTT_coq_002.v | 2 +- test-suite/bugs/closed/HoTT_coq_020.v | 4 ++-- 3 files changed, 40 insertions(+), 3 deletions(-) create mode 100644 test-suite/bugs/closed/4503.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v new file mode 100644 index 0000000000..f54d6433d8 --- /dev/null +++ b/test-suite/bugs/closed/4503.v @@ -0,0 +1,37 @@ +Require Coq.Classes.RelationClasses. + +Class PreOrder (A : Type) (r : A -> A -> Type) : Type := +{ refl : forall x, r x x }. + +(* FAILURE 1 *) + +Section foo. + Polymorphic Universes A. + Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + + Fail Definition foo := PO. +End foo. + + +Module ILogic. + +Set Universe Polymorphism. + +(* Logical connectives *) +Class ILogic@{L} (A : Type@{L}) : Type := mkILogic +{ + lentails: A -> A -> Prop; + lentailsPre:> RelationClasses.PreOrder lentails +}. + + +End ILogic. + +Set Printing Universes. + +(* There is stil a problem if the class is universe polymorphic *) +Section Embed_ILogic_Pre. + Polymorphic Universes A T. + Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. + +End Embed_ILogic_Pre. \ No newline at end of file diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v index ba69f6b158..dba4d5998f 100644 --- a/test-suite/bugs/closed/HoTT_coq_002.v +++ b/test-suite/bugs/closed/HoTT_coq_002.v @@ -9,7 +9,7 @@ Section SpecializedFunctor. (* Variable objC : Type. *) Context `(C : SpecializedCategory objC). - Polymorphic Record SpecializedFunctor := { + Record SpecializedFunctor := { ObjectOf' : objC -> Type; ObjectC : Object C }. diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 4938b80f9b..008fb72c4e 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -59,8 +59,8 @@ Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C := Build_Functor Cat0 C (fun x => match x with end). Section Law0. - Variable objC : Type. - Variable C : Category objC. + Polymorphic Variable objC : Type. + Polymorphic Variable C : Category objC. Set Printing All. Set Printing Universes. -- cgit v1.2.3 From 4b1103dc38754917e12bf04feca446e02cf55f07 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 24 Jan 2016 12:17:21 +0100 Subject: Fixing bug #4511: evar tactic can create non-typed evars. --- test-suite/bugs/closed/4511.v | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test-suite/bugs/closed/4511.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4511.v b/test-suite/bugs/closed/4511.v new file mode 100644 index 0000000000..0cdb3aee4f --- /dev/null +++ b/test-suite/bugs/closed/4511.v @@ -0,0 +1,3 @@ +Goal True. +Fail evar I. + -- cgit v1.2.3 From cb30837323aa462df24ad6668790f67b9bf20b5d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 24 Jan 2016 12:35:49 +0100 Subject: Fixing bug #4495: Failed assertion in metasyntax.ml. We simply handle the "break" in error messages. Not sure it is the proper bugfix though, we may want to be able to add breaks in such recursive notations. --- test-suite/bugs/closed/4495.v | 1 + 1 file changed, 1 insertion(+) create mode 100644 test-suite/bugs/closed/4495.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4495.v b/test-suite/bugs/closed/4495.v new file mode 100644 index 0000000000..8b032db5f5 --- /dev/null +++ b/test-suite/bugs/closed/4495.v @@ -0,0 +1 @@ +Fail Notation "'forall' x .. y ',' P " := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder). -- cgit v1.2.3 From e7852396a452f446135183ec3e1743b731d781c0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 24 Jan 2016 14:18:40 +0100 Subject: Adding a test for bug #4378. --- test-suite/bugs/closed/4378.v | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 test-suite/bugs/closed/4378.v (limited to 'test-suite') diff --git a/test-suite/bugs/closed/4378.v b/test-suite/bugs/closed/4378.v new file mode 100644 index 0000000000..9d59165562 --- /dev/null +++ b/test-suite/bugs/closed/4378.v @@ -0,0 +1,9 @@ +Tactic Notation "epose" open_constr(a) := + let a' := fresh in + pose a as a'. +Tactic Notation "epose2" open_constr(a) tactic3(tac) := + let a' := fresh in + pose a as a'. +Goal True. + epose _. Undo. + epose2 _ idtac. -- cgit v1.2.3