-
Notifications
You must be signed in to change notification settings - Fork 0
/
_CoqProject
79 lines (75 loc) · 2.4 KB
/
_CoqProject
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
-R ./lib/ixfree/src/IxFree Top.IxFree
-R ./lib/cpdt/src/Cpdt Top.Cpdt
-R ./coq-src/ABS Top.ABS
-R ./lib/tlc/src TLC
coq-src/ABS/Util/Foreach.v
coq-src/ABS/Util/Wf_natnat.v
coq-src/ABS/Util/Subset.v
coq-src/ABS/Util/Postfix.v
coq-src/ABS/Util/FromList.v
coq-src/ABS/Util/Tactics.v
coq-src/ABS/Lang/Syntax.v
coq-src/ABS/Lang/Bindings_Xs.v
coq-src/ABS/Lang/Bindings_map.v
coq-src/ABS/Lang/Bindings_bind.v
coq-src/ABS/Lang/Bindings.v
coq-src/ABS/Lang/Operational.v
coq-src/ABS/Lang/BindingsFacts_Xs.v
coq-src/ABS/Lang/BindingsFacts_map_0.v
coq-src/ABS/Lang/BindingsFacts_map_1.v
coq-src/ABS/Lang/BindingsFacts_map_2.v
coq-src/ABS/Lang/BindingsFacts_map_3.v
coq-src/ABS/Lang/BindingsFacts_map_4.v
coq-src/ABS/Lang/BindingsFacts_map_5.v
coq-src/ABS/Lang/BindingsFacts_map.v
coq-src/ABS/Lang/BindingsFacts_bind_0.v
coq-src/ABS/Lang/BindingsFacts_bind_1.v
coq-src/ABS/Lang/BindingsFacts_bind_2.v
coq-src/ABS/Lang/BindingsFacts_bind_3.v
coq-src/ABS/Lang/BindingsFacts_bind_4.v
coq-src/ABS/Lang/BindingsFacts_bind_5.v
coq-src/ABS/Lang/BindingsFacts_bind_6.v
coq-src/ABS/Lang/BindingsFacts_bind_7.v
coq-src/ABS/Lang/BindingsFacts_bind.v
coq-src/ABS/Lang/BindingsFacts.v
coq-src/ABS/Lang/OperationalFacts.v
coq-src/ABS/Lang/Sim.v
coq-src/ABS/Lang/SimFacts.v
coq-src/ABS/Lang/Static.v
coq-src/ABS/Lang/StaticFacts.v
coq-src/ABS/Lang/StaticFacts_0.v
coq-src/ABS/Lang/StaticFacts_1.v
coq-src/ABS/Lang/StaticFacts_2.v
coq-src/ABS/Lang/StaticFacts_3.v
coq-src/ABS/Lang/Context.v
coq-src/ABS/Rel/Definitions_closed.v
coq-src/ABS/Rel/Definitions_unfold.v
coq-src/ABS/Rel/Definitions_open.v
coq-src/ABS/Rel/Definitions.v
coq-src/ABS/Rel/BasicFacts.v
coq-src/ABS/Rel/Compat_sub.v
coq-src/ABS/Rel/Compat_weaken_X.v
coq-src/ABS/Rel/Compat_map_EV.v
coq-src/ABS/Rel/Compat_map_HV.v
coq-src/ABS/Rel/Compat_map.v
coq-src/ABS/Rel/Compat_bind_EV.v
coq-src/ABS/Rel/Compat_bind_HV.v
coq-src/ABS/Rel/Compat_hd_def.v
coq-src/ABS/Rel/Compat_hd_var.v
coq-src/ABS/Rel/Compat_val_up.v
coq-src/ABS/Rel/Compat_val_efun.v
coq-src/ABS/Rel/Compat_val_hfun.v
coq-src/ABS/Rel/Compat_val_fun.v
coq-src/ABS/Rel/Compat_val_var.v
coq-src/ABS/Rel/Compat_val_unit.v
coq-src/ABS/Rel/Compat_tm_val.v
coq-src/ABS/Rel/Compat_tm_let.v
coq-src/ABS/Rel/Compat_tm_app.v
coq-src/ABS/Rel/Compat_tm_eapp.v
coq-src/ABS/Rel/Compat_tm_happ.v
coq-src/ABS/Rel/Compat_tm_down.v
coq-src/ABS/Rel/Compat.v
coq-src/ABS/Rel/Adequacy.v
coq-src/ABS/Rel/Parametricity.v
coq-src/ABS/Rel/TypeSafety.v
coq-src/ABS/Rel/Soundness.v