Bug#340185: coq: FTBFS: implementation doesn't match interface: parsing/pcoq*

[Roland Stigge <stigge@antcom.de>]

Package: coq
Version: 8.0pl2-3
Severity: serious

Hi,

building the package coq in a clean sid build environment
(with pbuilder) on i386 results in:

=========================================================================
[...]
OCAMLC    interp/coqlib.mli
OCAMLC    interp/coqlib.ml
OCAMLC    library/declare.mli
OCAMLC    library/declare.ml
OCAMLC -a -o interp/interp.cma
OCAMLC    parsing/coqast.ml
OCAMLC    parsing/ast.mli
OCAMLC    parsing/ast.ml
OCAMLC    parsing/termast.mli
OCAMLC    parsing/termast.ml
OCAMLC    parsing/extend.mli
OCAMLC    parsing/extend.ml
OCAMLC    parsing/esyntax.mli
OCAMLC    parsing/esyntax.ml
OCAMLC    -rectypes proofs/tacexpr.ml
OCAMLC    toplevel/vernacexpr.ml
OCAMLC    parsing/pcoq.mli
OCAMLC4   parsing/pcoq.ml4
Warning: pa_ifdef is deprecated since OCaml 3.07. Use pa_macro instead.
File "parsing/pcoq.ml4", line 620, characters 4-18:
Warning Y: unused variable l'.
The implementation parsing/pcoq.ml4
does not match the interface parsing/pcoq.cmi:
Values do not match:
  val main_entry : ((Coqast.t -> Util.loc) * '_a) option Gram.Entry.e
is not included in
  val main_entry : (Util.loc * Vernacexpr.vernac_expr) option Gram.Entry.e
make[1]: *** [parsing/pcoq.cmo] Error 2
make[1]: Leaving directory `/tmp/buildd/coq-8.0pl2'
make: *** [build-stamp] Error 2
=========================================================================

Thanks for considering.


--
DARTS - Debian Archive Regression Test Suite
http://darts.alioth.debian.org/