# Those are actual and useful file names
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_abbreviation_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_axiom_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_constructor_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_definition_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_global_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_inductive_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_instance_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_lemma_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_library_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_module_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_notation_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_projection_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_record_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_section_*.html]
mathcomp-doc: file-name-contains-wildcard-character [usr/share/doc/mathcomp-doc/htmldoc/index_variable_*.html]
