diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /test-suite/bugs/closed/4503.v | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'test-suite/bugs/closed/4503.v')
-rw-r--r-- | test-suite/bugs/closed/4503.v | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v new file mode 100644 index 00000000..f54d6433 --- /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 |