-Q theories stdpp # "Declare Scope" does not exist yet in 8.9 -arg -w -arg -undeclared-scope theories/base.v theories/tactics.v theories/option.v theories/fin_map_dom.v theories/boolset.v theories/fin_maps.v theories/fin.v theories/vector.v theories/pmap.v theories/stringmap.v theories/fin_sets.v theories/mapset.v theories/proof_irrel.v theories/hashset.v theories/pretty.v theories/countable.v theories/orders.v theories/natmap.v theories/strings.v theories/relations.v theories/sets.v theories/listset.v theories/streams.v theories/gmap.v theories/gmultiset.v theories/prelude.v theories/listset_nodup.v theories/finite.v theories/numbers.v theories/nmap.v theories/zmap.v theories/coPset.v theories/lexico.v theories/propset.v theories/decidable.v theories/list.v theories/functions.v theories/hlist.v theories/sorting.v theories/infinite.v theories/nat_cancel.v theories/namespaces.v theories/telescopes.v