_CoqProject.test-suite

-arg -w -arg -redundant-canonical-projection
-arg -w -arg -projection-no-head-constant
-arg -w -arg -abstract-large-number
-arg -w -arg -disj-pattern-notation
-arg -w -arg -notation-overridden

examples/readme.v
examples/hulk.v

examples/demo1/hierarchy_0.v
examples/demo1/hierarchy_1.v
examples/demo1/hierarchy_2.v
examples/demo1/hierarchy_3.v
examples/demo1/hierarchy_4.v
examples/demo1/hierarchy_5.v
examples/demo1/test_0_0.v
examples/demo1/test_1_0.v
examples/demo1/test_2_0.v
examples/demo1/test_3_0.v
examples/demo1/test_3_3.v
examples/demo1/test_4_0.v
examples/demo1/test_4_3.v
examples/demo1/test_5_0.v
examples/demo1/test_5_3.v

examples/demo2/classical.v
examples/demo2/stage10.v
examples/demo2/stage11.v

examples/demo3/hierarchy_0.v
examples/demo3/hierarchy_1.v
examples/demo3/hierarchy_2.v
examples/demo3/test_0_0.v
examples/demo3/test_1_0.v
examples/demo3/test_2_0.v

examples/demo4/hierarchy_0.v

examples/demo5/hierarchy_0.v

examples/FSCD2020_material/V1.v
examples/FSCD2020_material/V2.v
examples/FSCD2020_material/V3.v
examples/FSCD2020_material/V4.v

examples/FSCD2020_talk/V1.v
examples/FSCD2020_talk/V2.v
examples/FSCD2020_talk/V3.v

examples/Coq2020_material/CoqWS_demo.v
examples/Coq2020_material/CoqWS_abstract.v
examples/Coq2020_material/CoqWS_expansion/withHB.v
examples/Coq2020_material/CoqWS_expansion/withoutHB.v

tests/type_of_exported_ops.v
tests/duplicate_structure.v
tests/instance_params_no_type.v
tests/test_CS_db_filtering.v
tests/subtype.v
tests/infer.v
tests/exports.v
tests/exports2.v
tests/log_impargs_record.v
tests/compress_coe.v
tests/funclass.v
tests/grefclass.v
tests/local_instance.v
tests/lock.v
tests/interleave_context.v
tests/not_same_key.v
#tests/factory_sort.v
tests/hb_pack.v
tests/declare.v
tests/short.v
tests/primitive_records.v
tests/non_forgetful_inheritance.v
tests/fix_loop.v
tests/test_synthesis_params.v
tests/hnf.v
tests/fun_instance.v
tests/issue284.v
tests/issue287.v

-R tests HB.tests
-R examples HB.examples

-Q . HB