The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

Given vec the type of lists of length n (given in appendix), I am in
this situation:

m   : nat
v   : vec Prop (S m)
IHm : vec Prop (m) -> Prop
==================
Prop

I'd like to destruct v into vcons a v', in order to do:
 exact (a -> (IHm v')).

But then I get this anomaly:

> destruct v.
> ^^^^^^^^^^
Anomaly: Cannot take the successor of a non variable universes: you
are probably typing a type already known to be the type of a
user-provided term; if you really need this, please report.  Please
report.

So, can _somebody_ explain me _what_ this says and maybe even how I
can avoid the situation?

Thanks in advance.


APPENDIX
========

Inductive vec : Type -> nat -> Type :=
  | vnil  : forall A:Type, vec A 0
  | vcons : forall A:Type, forall n:nat, A -> vec A n -> vec A (S n).


-- 
Lionel