diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:13:01 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:13:01 +0200 |
commit | d18b6226c9ecdb0ebbef6d29fb9f0c09ba78a5fa (patch) | |
tree | f9a2c15acb3448f4e78f4e8b7328f751fb144aa0 /test-suite/bugs/closed/shouldsucceed/1865.v | |
parent | 4892a9c7ae62f552fa42701788b2bd08a7f3bc08 (diff) | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Merge commit 'upstream/8.2.beta3+dfsg'
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1865.v')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1865.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1865.v b/test-suite/bugs/closed/shouldsucceed/1865.v new file mode 100644 index 00000000..17c19989 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1865.v @@ -0,0 +1,18 @@ +(* Check that tactics (here dependent inversion) do not generate + conversion problems T <= U with sup's of universes in U *) + +(* Submitted by David Nowak *) + +Inductive list (A:Set) : nat -> Set := +| nil : list A O +| cons : forall n, A -> list A n -> list A (S n). + +Definition f (n:nat) : Type := + match n with + | O => bool + | _ => unit + end. + +Goal forall A n, list A n -> f n. +intros A n. +dependent inversion n. |