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
