-
Notifications
You must be signed in to change notification settings - Fork 26
/
.gitignore
141 lines (141 loc) · 4.1 KB
/
.gitignore
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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
*.vo
*.vok
*.vos
*.v.d
*.glob
*.aux
*.out
*.html
*.cache
*.cm*
*.o
*.a
*.ml*.d
*.vok
*.vos
Makefile.coq
/libraries/Makefile
/theories/Makefile
/theories/Makefile.plugin
/theories/Extraction/*.ml
/theories/Extraction/*.mli
/theories/ExtractionVanilla/*.ml
/theories/ExtractionVanilla/*.mli
/theories/*.ml
/theories/*.mli
.coqdeps.d
.DS_Store
*.bak
Makefile.conf
Makefile.plugin.conf
/plugin/Makefile
/plugin/extraction
/cplugin/extraction
/cplugin/Makefile
theories/.coqdeps.d
libraries/.coqdeps.d
myMain.ml
myMain.mli
vs.ml
vs.mli
benchmarks/mod.py
benchmarks/demo1
benchmarks/demo2
benchmarks/CertiCoq.Benchmarks.*.c
benchmarks/CertiCoq.Benchmarks.*.h
test_plugin.*.c
test_plugin.*.h
benchmarks/config.h
benchmarks/gc.h
benchmarks/values.h
benchmarks/main.c
theories/.Makefile.d
libraries/.Makefile.d
benchmarks/vs
plugin/.Makefile.d
CertiCoq.Benchmarks.Binom.main.c
CertiCoq.Benchmarks.Binom.main.h
plugin/g_certicoq.ml
benchmarks/lib/.Makefile.d
CertiCoq.Benchmarks.lib.Binom.main.c
CertiCoq.Benchmarks.lib.Binom.main.h
glue.CertiCoq.Benchmarks.lib.Binom.main.c
glue.CertiCoq.Benchmarks.lib.Binom.main.h
benchmarks/binom_opt
benchmarks/binom_opt_ll
benchmarks/color_opt
benchmarks/color_opt_ll
benchmarks/demo1_opt
benchmarks/demo1_opt_ll
benchmarks/demo2_opt
benchmarks/demo2_opt_ll
benchmarks/list_sum_opt
benchmarks/list_sum_opt_ll
benchmarks/ocamlc_bench_1.txt
benchmarks/ocamlopt_bench_1.txt
benchmarks/sha_fast
benchmarks/sha_fast_opt
benchmarks/sha_fast_opt_ll
benchmarks/vs_easy_opt
benchmarks/vs_easy_opt_ll
benchmarks/vs_hard_opt
benchmarks/vs_hard_opt_ll
benchmarks/glue_*.c
benchmarks/glue_*.h
benchmarks/glue.CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.c
benchmarks/glue.CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.h
benchmarks/metacoq_erasure/CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.metacoq_erasure.c
benchmarks/metacoq_erasure/CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.metacoq_erasure.h
benchmarks/metacoq_erasure/g_safe_erasure.ml
benchmarks/metacoq_erasure/glue.CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.metacoq_erasure.c
benchmarks/metacoq_erasure/glue.CertiCoq.Benchmarks.metacoq_erasure.metacoq_erasure.metacoq_erasure.h
benchmarks/metacoq_erasure/metacoq_erasure
cplugin/g_certicoq_vanilla.ml
bootstrap/certicoq_pipeline/g_certicoqc.ml
bootstrap/certicoqc/CertiCoq.CertiCoqC.compile.certicoqc.c
bootstrap/certicoqc/CertiCoq.CertiCoqC.compile.certicoqc.h
bootstrap/certicoqc/glue.CertiCoq.CertiCoqC.compile.certicoqc.c
bootstrap/certicoqc/glue.CertiCoq.CertiCoqC.compile.certicoqc.h
bootstrap/certicoqc/g_certicoqc.ml
bootstrap/certicoqchk/CertiCoq.CertiCoqCheck.compile.certicoqchk.c
bootstrap/certicoqchk/CertiCoq.CertiCoqCheck.compile.certicoqchk.h
bootstrap/certicoqchk/glue.CertiCoq.CertiCoqCheck.compile.certicoqchk.c
bootstrap/certicoqchk/glue.CertiCoq.CertiCoqCheck.compile.certicoqchk.h
bootstrap/certicoqchk/g_certicoqchk.ml
bootstrap/Makefile
bootstrap/certicoqc/tests/CertiCoq.CertiCoqC.compile.certicoqc.c
bootstrap/certicoqc/tests/CertiCoq.CertiCoqC.compile.certicoqc.h
bootstrap/certicoqc/tests/glue.CertiCoq.CertiCoqC.compile.certicoqc.c
bootstrap/certicoqc/tests/glue.CertiCoq.CertiCoqC.compile.certicoqc.h
compile.certicoqchk.ir
benchmarks/test_primitive
bootstrap/certicoqc/.Makefile.certicoqc.d
bootstrap/certicoqc/Makefile.certicoqc
bootstrap/certicoqc/Makefile.certicoqc.conf
bootstrap/certicoqc/tests/test.certicoqc*
cplugin/.Makefile.d
tests/glue.test.certicoqc.c
tests/glue.test.certicoqc.h
tests/test.certicoqc.c
tests/test.certicoqc.h
bootstrap/certicoqc/tests/glue.test.certicoqc.c
bootstrap/certicoqc/tests/glue.test.certicoqc.h
bootstrap/certicoqchk/.Makefile.certicoqchk.d
bootstrap/certicoqchk/Makefile.certicoqchk
bootstrap/certicoqchk/Makefile.certicoqchk.conf
cplugin/META
plugin/META
_opam
bootstrap/certicoqc/META
bootstrap/certicoqchk/META
bootstrap/certicoqc*/glue.c
bootstrap/certicoqc*/glue.h
plugin/.merlin
_build
.vscode/CertiCoq.code-workspace
bootstrap/certicoqc/CertiCoq.CertiCoqC.CertiCoqC.certicoqc.c
bootstrap/certicoqc/CertiCoq.CertiCoqC.CertiCoqC.certicoqc.h
bootstrap/certicoqc/tests/test.demo1.c
bootstrap/certicoqc/tests/test.demo1.h
plugin/.filestoinstall
cplugin/.merlin