1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
|
-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
-arg -w -arg +elpi.typecheck
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
# examples/cat/cat.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/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/instance_before_structure.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
tests/two_hier.v
tests/instance_merge_with_param.v
tests/instance_merge_with_distinct_param.v
tests/instance_merge.v
tests/unit/enrich_type.v
tests/unit/mixin_src_has_mixin_instance.v
tests/unit/mk_src_map.v
tests/unit/close_hole_term.v
tests/unit/struct.v
tests/factory_when_notation.v
tests/saturate_on.v
tests/bug_435.v
tests/bug_447.v
tests/unimported_relevant_class.v
tests/unimported_irrelevant_class.v
-R tests HB.tests
-R examples HB.examples
-Q HB HB
|
