From 784d82dc1a709c4c262665a4cd4eb0b1bd1487a0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Jun 2016 18:36:58 +0200 Subject: Univs: fix for part #2 of bug #4816. Check that the polymorphic status of everything that is parameterized in nested sections is coherent. --- test-suite/bugs/closed/4816.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 test-suite/bugs/closed/4816.v (limited to 'test-suite/bugs/closed/4816.v') diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v new file mode 100644 index 000000000..ef79b9869 --- /dev/null +++ b/test-suite/bugs/closed/4816.v @@ -0,0 +1,18 @@ +Section foo. +Polymorphic Universes A B. +Constraint A <= B. +End foo. +(* gives an anomaly Universe undefined *) + +or even, a refinement of #4503: +Require Coq.Classes.RelationClasses. + +Class PreOrder (A : Type) (r : A -> A -> Type) : Type := +{ refl : forall x, r x x }. + +Section foo. + Polymorphic Universes A. + Section bar. + Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + End bar. +End foo. \ No newline at end of file -- cgit v1.2.3 From 3bb0753d1589489b0e33f6a116a84c4fa72ed49f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Jun 2016 22:28:14 +0200 Subject: Fix test-suite file, only part 2 is fixed in 8.5 --- test-suite/bugs/closed/4816.v | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) (limited to 'test-suite/bugs/closed/4816.v') diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v index ef79b9869..5ba0787ee 100644 --- a/test-suite/bugs/closed/4816.v +++ b/test-suite/bugs/closed/4816.v @@ -1,10 +1,3 @@ -Section foo. -Polymorphic Universes A B. -Constraint A <= B. -End foo. -(* gives an anomaly Universe undefined *) - -or even, a refinement of #4503: Require Coq.Classes.RelationClasses. Class PreOrder (A : Type) (r : A -> A -> Type) : Type := @@ -13,6 +6,6 @@ Class PreOrder (A : Type) (r : A -> A -> Type) : Type := Section foo. Polymorphic Universes A. Section bar. - Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. End bar. End foo. \ No newline at end of file -- cgit v1.2.3