test-suite/bugs/closed/4670.v


1
2
3
4
5
6
7

Require Import Coq.Vectors.Vector.
Module Bar.
  Definition foo A n (l : Vector.t A n) : True.
  Proof.
    induction l ; exact I.
  Defined.
End Bar.