diff options
| author | Matthieu Sozeau | 2015-11-02 13:48:53 -0500 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-02 16:23:15 -0500 |
| commit | 739d8e50b3681491bd82b516dbbba892ac5b424b (patch) | |
| tree | 1df539e5128d1a51f63863ca04def121f5e9591b /test-suite | |
| parent | 5a5f2b4253b5834e09f43cb36a81ce6f53cc2da3 (diff) | |
Refresh rigid universes as well, and in 8.4 compatibility mode,
make them rigid to disallow minimization.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4394.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v new file mode 100644 index 0000000000..751f1e697d --- /dev/null +++ b/test-suite/bugs/closed/4394.v @@ -0,0 +1,13 @@ +(* -*- 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. +Definition Family := Type -> Type. +Definition fooFamily family : Family := Foo family. +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 |