diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_11722.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_11722.v b/test-suite/bugs/closed/bug_11722.v new file mode 100644 index 0000000000..d4bd5f48b2 --- /dev/null +++ b/test-suite/bugs/closed/bug_11722.v @@ -0,0 +1,20 @@ +Require Import Program. +Set Universe Polymorphism. + +Inductive paths@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := + idpath : paths A a a. + +Inductive nat := + | O : nat + | S : nat -> nat. + +Axiom cheat : forall {A}, A. + +Program Definition foo@{i} : forall x : nat, paths@{i} nat x x := _. +Next Obligation. + destruct x. + constructor. + apply cheat. +Defined. (* FIXED: Universe unbound error *) + +Check foo@{_}. |