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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
*.glob
*.d
*.d.raw
*.vos
*.vok
*.vo
*.cm*
*.annot
*.spit
*.spot
*.o
*.a
*.pyc
*.log
*.aux
*.dvi
*.pdf
*.blg
*.bbl
*.idx
*.ilg
*.toc
*.atoc
*.comidx
*.comind
*.erridx
*.errind
*.haux
*.hcomind
*.herrind
*.hind
*.htacind
*.htoc
*.ind
*.lof
*.tacidx
*.tacind
*.v.tex
*.v.ps
*.v.timing
*.v.timing.diff
*.v.before-timing
*.v.after-timing
*.v.html
*.stamp
*.native
revision
TAGS
.DS_Store
.pc
_build
_build_vo
_build_ci
_install_ci
config/Makefile
config/coq_config.ml
config/coq_byte_config.ml
config/coq_config.py
config/dune.c_flags
ide/coqide/config.ml
dev/ocamldebug-coq
time-of-build*.log
time-of-build*.log2
time-of-build*.log3
.csdp.cache
test-suite/.lia.cache
test-suite/.nra.cache
test-suite/.nia.cache
test-suite/trace
test-suite/misc/universes/all_stdlib.v
test-suite/misc/universes/universes.txt
test-suite/coq-makefile/*/actual
test-suite/coq-makefile/*/desired
test-suite/coq-makefile/**/*.processed
test-suite/coq-makefile/**/Makefile
test-suite/coq-makefile/**/Makefile.conf
test-suite/coq-makefile/*/src
test-suite/coq-makefile/*/theories
test-suite/coq-makefile/*/theories2
test-suite/coq-makefile/*/html
test-suite/coq-makefile/*/mlihtml
test-suite/coq-makefile/*/subdir/done
test-suite/coq-makefile/merlin1/.merlin
test-suite/coqdoc/Coqdoc.*
test-suite/coqdoc/index.html
test-suite/coqdoc/coqdoc.css
test-suite/output/MExtraction.out
test-suite/output/*.out.real
test-suite/oUnit-anon.cache
test-suite/redirect_test.out
test-suite/unit-tests/**/*.test
test-suite/ide/fake_ide.exe
test-suite/Datatypes.ml
test-suite/Datatypes.mli
test-suite/bug_10796.ml
test-suite/bug_10796.mli
test-suite/**/*.time
stdlib/test-suite/**/*.time
# `nix build` (through flake) symlink
result
# documentation
doc/common/version.tex
doc/faq/html/
doc/faq/axioms.eps
doc/faq/axioms.eps_t
doc/faq/axioms.pdf_t
doc/faq/axioms.png
doc/sphinx/index.rst
doc/sphinx/zebibliography.rst
doc/corelib/Library.out
doc/corelib/Library.ps
doc/corelib/Library.coqdoc.tex
doc/corelib/FullLibrary.ps
doc/corelib/FullLibrary.coqdoc.tex
doc/corelib/html/
doc/corelib/index-body.html
doc/corelib/index-list.html
doc/tools/docgram/editedGrammar
doc/tools/docgram/prodnGrammar
doc/tools/docgram/prodnCommands
doc/tools/docgram/prodnTactics
doc/tools/docgram/updated_rsts
# other auto-generated files
ide/coqide/default.bindings
ide/coqide/default_bindings_src.exe
ide/coqide/index_urls.txt
.lia.cache
.nia.cache
.nra.cache
theories/Makefile.coq
theories/Makefile.coq.conf
# emacs save files
*~
\#*\#
# vscode local config
.vscode/
# coqide generated files (when testing)
*.crashcoqide
.*.sw*
.#*
ide/coqide/coqide.keys
.dune.lock
# bin compat directory, should be eventually be phased out
bin
# generated by dune build -p
*.install
.dune-stamp
theories/dune
user-contrib/Ltac2/dune
/test-suite/test_suite_config.inc
.wrappers
rocq-stdlib-doc.opam
doc/stdlib/Library.fdb_latexmk
doc/stdlib/Library.fls
|
