diff options
author | 2015-11-13 11:43:34 +0100 | |
---|---|---|
committer | 2015-11-13 11:43:34 +0100 | |
commit | 4e76c4f01b69b77f40686e06c4544aa156efaa5a (patch) | |
tree | aefad2e3de35f75c46729f9310d33b56d3821961 /test-suite/success/polymorphism.v | |
parent | 64fa31c7ee53e79b112507fb2eea27dc7648328d (diff) | |
parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'test-suite/success/polymorphism.v')
-rw-r--r-- | test-suite/success/polymorphism.v | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 9167c9fc..d6bbfe29 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -1,3 +1,5 @@ +Unset Strict Universe Declaration. + Module withoutpoly. Inductive empty :=. @@ -292,3 +294,31 @@ Section foo2. Context `{forall A B, Funext A B}. Print Universes. End foo2. + +Module eta. +Set Universe Polymorphism. + +Set Printing Universes. + +Axiom admit : forall A, A. +Record R := {O : Type}. + +Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}. +Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl. +Definition RLRL' : forall x : R, RL x = RL (RL x). + intros. apply eq_refl. +Qed. + +End eta. + +Module Hurkens'. + Require Import Hurkens. + +Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. + +Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. + +Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ +Type)) eq_refl. + +End Hurkens'.
\ No newline at end of file |