aboutsummaryrefslogtreecommitdiffstats
path: root/.gitignore
blob: 7889af6c01cc73dcd630b99832303812f6844e64 (plain)
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
# Object files, in general
**#*#
**.swp
**.bin
**.out
**.tok
*.vo
*.vok
*.vos
*.glob
*.o
*.a
*.cmi
*.cmo
*.cmx
*.cma
*.cmxa
.*.aux
*.cmti
*.cmt
# Emacs saves
*~
# Executables and configuration
/tools/compiler_expand
/ccomp
/ccomp.byte
/ccomp.prof
/clightgen
/clightgen.byte
/tools/ndfun
/tools/modorder
/Makefile.config
/.merlin
/_CoqProject
/compile.pl
# Generated files
/.depend
/.depend.extr
/compcert.ini
/compcert.config
/x86/ConstpropOp.v
/x86/SelectOp.v
/x86/SelectLong.v
/powerpc/ConstpropOp.v
/powerpc/SelectOp.v
/powerpc/SelectLong.v
/arm/ConstpropOp.v
/arm/SelectOp.v
/arm/SelectLong.v
/riscV/ConstpropOp.v
/riscV/SelectOp.v
/riscV/SelectLong.v
/kvx/ConstpropOp.v
/kvx/SelectOp.v
/kvx/SelectLong.v
/aarch64/ConstpropOp.v
/aarch64/SelectOp.v
/aarch64/SelectLong.v
/backend/SelectDiv.v
/backend/SplitLong.v
/cparser/Parser.v
/cparser/Lexer.ml
/cparser/pre_parser.ml
/cparser/pre_parser.mli
/cparser/pre_parser_messages.ml
/cparser/pre_parser.automaton
/cparser/pre_parser.messages
/cparser/pre_parser.conflicts
/cparser/handcrafted.messages.bak
/cparser/handcrafted.messages.raw
/cparser/deLexer
/cparser/tests/generated/*.c
/cparser/tests/generated/*.err
/lib/Readconfig.ml
/lib/Tokenize.ml
/lib/Responsefile.ml
/driver/Version.ml
/driver/Compiler.v
/extraction/extraction.v
# Documentation
/doc/coq2html
/doc/coq2html.ml
/doc/html
/doc/html/
# MacOS metadata
.DS_Store
runtime/kvx/i64_sdiv.s
runtime/kvx/i64_smod.s
runtime/kvx/i64_udiv.s
runtime/kvx/i64_udivmod.s
runtime/kvx/i64_umod.s
# Test generated data
/test/export/clight/*.v
/test/export/csyntax/*.v
# Coq caches
.lia.cache
.nia.cache
.nra.cache
.csdp.cache