The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

hello! could anyone explain me why, in the following code, the first
definition is accepted, while the second one is not? is it normal or is it a
bug? thanks.

Require Export Bvector.

  Definition var := nat.
  Definition symb := nat.

  Variable arity : symb -> nat.

  Inductive term : Set :=
    | Var : var -> term
    | Fun : forall f : symb, vector term (arity f) -> term.

  Variable A : Set.
  Variable xint : var -> A.
  Variable fint : forall f : symb, vector A (arity f) -> A.

  Fixpoint term_int (t : term) : A :=
    match t with
      | Var x => xint x
      | Fun f v =>
        let fix termvec_int (n : nat) (v : vector term n) { struct v }
            : (vector A n) :=
          match v in (vector _ n) return (vector A n) with
            | Vnil => Vnil A
            | Vcons t' n' v' => Vcons A (term_int t') n' (termvec_int n' v')
          end
        in fint f (termvec_int (arity f) v)
    end.

  Fixpoint term_int2 (t : term) : A :=
    match t with
      | Var x => xint x
      | Fun f v => fint f (termvec_int2 (arity f) v)
    end
  with termvec_int2 (n : nat) (v : vector term n) { struct v }
       : (vector A n) :=
    match v in (vector _ n) return (vector A n) with
      | Vnil => Vnil A
      | Vcons t' n' v' => Vcons A (term_int2 t') n' (termvec_int2 n' v')
    end.

(*
Error:
Recursive definition of termvec_int2 is ill-formed.
In environment
n : nat
v : vector term n
t' : term
n' : nat
v' : vector term n'
Recursive call to term_int2 has principal argument equal to t'
instead of v'
*)