.gitignore 3.19 KB
Newer Older
1
*.tmp
Claude Marche's avatar
Claude Marche committed
2
*~
MARCHE Claude's avatar
MARCHE Claude committed
3
*.bak
Francois Bobot's avatar
Francois Bobot committed
4
*.o
Simon Cruanes's avatar
Simon Cruanes committed
5
.*.swp
6
why.conf
7 8 9
*.cmx
*.cmo
*.cmi
François Bobot's avatar
François Bobot committed
10
*.cmxs
11
*.annot
François Bobot's avatar
François Bobot committed
12
\#*\#
13

Francois Bobot's avatar
Francois Bobot committed
14 15 16 17 18 19 20 21 22 23 24 25
# /
/config.status
/config.log
/autom4te.cache
/Makefile
/configure
/.depend.*
/semantic.cache
/TAGS
/output_why3
/output_coq
/dep.pdf
MARCHE Claude's avatar
MARCHE Claude committed
26 27
/distrib
/META
Francois Bobot's avatar
Francois Bobot committed
28

29 30 31 32 33 34 35 36 37
# /bench/
/bench/programs/good/booleans/
/bench/programs/good/exceptions/
/bench/programs/good/for/
/bench/programs/good/list/
/bench/programs/good/see/
/bench/programs/good/set/
/bench/programs/good/recfun/

Francois Bobot's avatar
Francois Bobot committed
38
# /bin/
39 40 41 42 43 44 45 46 47
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3ml.byte
/bin/why3ml.opt
/bin/why3ml
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
48
/bin/why3-cpulimit
49 50 51 52 53 54
/bin/why3config.byte
/bin/why3config.opt
/bin/why3config
/bin/why3bench.byte
/bin/why3bench.opt
/bin/why3bench
55 56
/bin/why3doc.byte
/bin/why3doc.opt
57
/bin/why3doc
58 59 60
/bin/why3replayer.byte
/bin/why3replayer.opt
/bin/why3replayer
Francois Bobot's avatar
Francois Bobot committed
61 62 63

# /doc/
/doc/version.tex
MARCHE Claude's avatar
MARCHE Claude committed
64
/doc/ocamldoc.sty
Francois Bobot's avatar
Francois Bobot committed
65 66 67 68
/doc/*whizzy*
/doc/manual.wdvi
/doc/manual.raux
/doc/manual.log
69
/doc/manual.lof
Francois Bobot's avatar
Francois Bobot committed
70 71 72 73 74 75 76
/doc/manual.toc
/doc/manual.aux
/doc/manual.bbl
/doc/manual.blg
/doc/manual.ind
/doc/manual.ilg
/doc/manual.idx
MARCHE Claude's avatar
MARCHE Claude committed
77
/doc/manual.rel
MARCHE Claude's avatar
MARCHE Claude committed
78 79 80 81
/doc/manual.glg
/doc/manual.glo
/doc/manual.gls
/doc/manual.ist
82
/doc/manual.out
Francois Bobot's avatar
Francois Bobot committed
83 84 85 86 87
/doc/*.haux
/doc/*.pdf
/doc/manual.html
/doc/*.hind
/doc/*.htoc
MARCHE Claude's avatar
MARCHE Claude committed
88 89 90
/doc/bnf
/doc/bnf.ml
/doc/*_bnf.tex
91 92
/doc/apidoc.tex
/doc/apidoc/*.html
Francois Bobot's avatar
Francois Bobot committed
93 94

# /share/
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
95
/share/provers-detection-data.conf
Francois Bobot's avatar
Francois Bobot committed
96 97 98
/share/emacs/semantic.cache

# /src/
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
99
/src/config.sh
Francois Bobot's avatar
Francois Bobot committed
100
/src/config.ml
101
/src/*.cma
Francois Bobot's avatar
Francois Bobot committed
102
/src/*.cmxa
103
/src/*.a
Francois Bobot's avatar
Francois Bobot committed
104 105 106 107 108 109 110 111

# /src/coq-plugin/
/src/coq-plugin/g_whytac.ml

# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
112
/src/driver/driver_parser.output
Francois Bobot's avatar
Francois Bobot committed
113 114 115 116 117

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
118 119
/src/parser/parser.pre.ml
/src/parser/parser.pre.mli
120
/src/parser/parser.pre.output
Francois Bobot's avatar
Francois Bobot committed
121 122

# /src/tptp2why/
123
/src/tptp2why/tptpLexer.ml
Francois Bobot's avatar
Francois Bobot committed
124
/src/tptp2why/tptpParser.ml
125 126
/src/tptp2why/tptpParser.mli
/src/tptp2why/tptpParser.output
Francois Bobot's avatar
Francois Bobot committed
127
/src/tptp2why/tptpParser.automaton
128
/src/tptp2why/tptpParser.conflicts
Francois Bobot's avatar
Francois Bobot committed
129

130 131 132
# /src/ide/
/src/ide/xml.ml

133 134 135
# /src/why3doc/
/src/why3doc/to_html.ml

Francois Bobot's avatar
Francois Bobot committed
136 137 138 139
# /src/util/
/src/util/rc.ml

# /tests/
140
/tests/test-jcf/
141
/tests/test-pgm-jcf/
MARCHE Claude's avatar
MARCHE Claude committed
142 143 144
/tests/test-claude/

# /examples/
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
145
/examples/my_cosine/
146
/examples/scottish-private-club/
MARCHE Claude's avatar
MARCHE Claude committed
147
/examples/hello_proof/
MARCHE Claude's avatar
MARCHE Claude committed
148
/examples/einstein/
149
/examples/genealogy/
MARCHE Claude's avatar
MARCHE Claude committed
150 151
/examples/programs/isqrt/
/examples/programs/course/
152
/examples/programs/wcet_hull/
153
/examples/programs/my_cosine/
154
/examples/programs/binary_search2/
155
/examples/programs/vacid_0_sparse_array/
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
156 157
/examples/programs/vacid_0_red_black_trees/
/examples/programs/vacid_0_red_black_trees_harness/
158 159 160 161 162 163 164
/examples/programs/next_digit_sum/
/examples/programs/vstte10_max_sum/
/examples/programs/vstte10_search_list/
/examples/programs/vstte10_aqueue/
/examples/programs/insertion_sort_list/
/examples/programs/mergesort_list/
/examples/programs/binary_search/
165
/examples/programs/same_fringe/
166
/examples/programs/quicksort/
167 168 169 170 171 172 173 174 175 176 177
/examples/programs/algo63/
/examples/programs/algo64/
/examples/programs/algo65/
/examples/programs/binary_search_c/
/examples/programs/bresenham/
/examples/programs/dijkstra/
/examples/programs/distance/
/examples/programs/flag/
/examples/programs/gcd_bezout/
/examples/programs/sf/
/examples/programs/vstte10_queens/
178

179
# modules
180
/modules/string/
181
/modules/stack/
182
/modules/queue/
183