diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4394.v | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v index 751f1e697d..60c9354597 100644 --- a/test-suite/bugs/closed/4394.v +++ b/test-suite/bugs/closed/4394.v @@ -1,13 +1,19 @@ (* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) + Require Import Equality List. -Unset Strict Universe Declaration. -Inductive Foo I A := foo (B : Type) : A -> I B -> Foo I A. +Inductive Foo (I : Type -> Type) (A : Type) : Type := +| foo (B : Type) : A -> I B -> Foo I A. Definition Family := Type -> Type. -Definition fooFamily family : Family := Foo family. +Definition FooToo : Family -> Family := Foo. +Definition optionize (I : Type -> Type) (A : Type) := option (I A). +Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A. +Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. +Definition barRec : Rec (optionize id) := {| rec := bar id |}. Inductive Empty {T} : T -> Prop := . Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) : Empty (a, b) -> False. Proof. intro e. dependent induction e. -Qed.
\ No newline at end of file +Qed. + |