The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Lionel,
 
> 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?

  This is what should be called a bug... Please send a complete
reproducible script to 
coq-bugs AT coq.inria.fr.

  Informal explanation: internally, anonymous "Type" universes are
algebraic universes built from zero, succ, max and universe
variables. The type inference algorithm expects as input a term with
universe variables only and it produces as output a type which
contains "Type" universes algebraically built from the original
universe variables, and the zero, succ and max universe
constructors. If a function in Coq (e.g. a tactic) fails to call the
type inference algorithm with terms satisfying the precondition
(i.e. only universe variables in the "Type" expressions of the term),
then the above anomaly is raised.
 
  Hugo