Bug#1005920: closed by Debian FTP Masters <ftpmaster@ftp-master.debian.org> (reply to Julien Puydt <jpuydt@debian.org>) (Bug#1005920: fixed in coq-doc 8.15.0-3)

[Andreas Beckmann <anbe@debian.org>]

With all these B-D added, the build fails for me now with

Running[3870]: (cd _build/default/doc && /usr/bin/env sphinx-build -q -W -b html sphinx refman-html)
Command [3870] exited with code 2:
$ (cd _build/default/doc && /usr/bin/env sphinx-build -q -W -b html sphinx refman-html)

Warning, treated as error:
/build/coq-doc-8.15.0/_build/default/doc/sphinx/index.rst:45:toctree contains reference to document 'zebibliography' that doesn't have a title: no link will be generated
ANTLR runtime and generated code versions disagree: 4.9.1!=4.7.2
Duplicate cmd name:  Extraction
Duplicate exn name:  Not equal
Duplicate exn name:  Not equal (due to universes)
Duplicate tacn name:  first (ssreflect)
Duplicate tacn name:  have
Duplicate tacn name:  move (ssreflect)
Duplicate tacn name:  apply (ssreflect)
Duplicate tacn name:  under
Duplicate tacn name:  over
Duplicate tacn name:  wlog
Duplicate tacn name:  set (ssreflect)
Duplicate tacn name:  unlock
Duplicate tacn name:  congr
Duplicate cmd name:  Hint View for apply
Duplicate cmd name:  Prenex Implicits
Duplicate exn name:  Not the right number of missing arguments
Duplicate exn name:  No such hypothesis in current goal
Duplicate exn name:  No such hypothesis
Duplicate exn name:  ‘ident’ is used in the hypothesis ‘ident’
Duplicate exn name:  No such hypothesis
Duplicate exn name:  No such hypothesis
Duplicate exn name:  ‘ident’ is already used
Duplicate exn name:  No such assumption
Duplicate exn name:  No focused proof (No proof-editing in progress)
Duplicate exn name:  Not an inductive product
Duplicate exn name:  No primitive equality found

Not sure what exactly causes the failure ...

Andreas