.gitignore

*.tmp
*~
*.bak
*.o
why3.conf
*.cmx
*.cmo
*.cmi
*.cmxs
*.annot
*.dep
*.vo
*.vd
*.glob
\#*\#

# /
/config.status
/config.log
/autom4te.cache
/Makefile
/configure
/semantic.cache
/TAGS
/output_why3
/output_coq
/dep.pdf
/distrib
/why3regtests.err
/why3regtests.out

# /lib-ocaml/why3/
/lib-ocaml/why3/META
/lib-ocaml/why3/why3.cm*
/lib-ocaml/why3/why3.a
/lib-ocaml/why3/why3ml.cm*
/lib-ocaml/why3/why3ml.a

# /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/
/bench/programs/good/loops/
/bench/programs/good/po/
/bench/valid/list/

# /bin/
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
/bin/why3-cpulimit
/bin/why3-cpulimit.exe
/bin/why3config.byte
/bin/why3config.opt
/bin/why3config
/bin/why3bench.byte
/bin/why3bench.opt
/bin/why3bench
/bin/why3doc.byte
/bin/why3doc.opt
/bin/why3doc
/bin/why3replayer.byte
/bin/why3replayer.opt
/bin/why3replayer
/bin/why3html.byte
/bin/why3html.opt
/bin/why3html
/bin/why3stats.byte
/bin/why3stats.opt
/bin/why3stats
/bin/why3session.opt
/bin/why3session.byte
/bin/why3session

# /doc/
/doc/version.tex
/doc/ocamldoc.sty
/doc/*whizzy*
/doc/manual.wdvi
/doc/manual.raux
/doc/manual.log
/doc/manual.lof
/doc/manual.toc
/doc/manual.aux
/doc/manual.bbl
/doc/manual.blg
/doc/manual.ind
/doc/manual.ilg
/doc/manual.idx
/doc/manual.rel
/doc/manual.glg
/doc/manual.glo
/doc/manual.gls
/doc/manual.ist
/doc/manual.out
/doc/*.haux
/doc/*.pdf
/doc/html/
/doc/*.hind
/doc/*.htoc
/doc/bnf
/doc/bnf.ml
/doc/*_bnf.tex
/doc/apidoc.tex
/doc/apidoc/
/doc/stdlibdoc/

# /share/
/share/provers-detection-data.conf
/share/emacs/semantic.cache

# /src/
/src/config.sh
/src/config.ml
/src/coq_config.ml
/src/*.cma
/src/*.cmxa
/src/*.a

# Coq tactic
/src/coq-tactic/coqCompat.ml
/src/coq-tactic/g_why3tac.ml
/src/coq-tactic/.why3-vo-*
/lib/coq-tactic/why3tac.cma

# PVS
.pvscontext
orphaned-proofs.prf
/lib/pvs/*/*.summary
pvsbin/

# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
/src/driver/driver_parser.output

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
/src/parser/parser.output

# /src/why3doc/
/src/why3doc/doc_lexer.ml

# /src/util/
/src/util/rc.ml

# /src/session
/src/session/xml.ml

# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
/plugins/tptp/tptp_parser.output

# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux

# /tests/
/tests/test-jcf/
/tests/test-pgm-jcf/
/tests/test-claude/
/tests/test-and/

# /examples/
/examples/programs/course/
/examples/programs/wcet_hull/
/examples/programs/binary_search2/
/examples/programs/vacid_0_red_black_trees_harness/
/examples/programs/next_digit_sum/
/examples/programs/binary_search_c/
/examples/programs/dijkstra/
/examples/why3bench.html
/examples/why3regtests.err
/examples/why3regtests.out
/examples/*/*.html
/examples/*/*/*.html
/examples/*/*/*/*.html
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex

# modules
/modules/string/
/modules/stack/
/modules/queue/
/modules/pqueue/