*.tmp
*~
*.bak
*.o
*.a
why3.conf
*.cmx
*.cmo
*.cmi
*.cmxs
*.cma
*.cmxa
*.cmt
*.cmti
*.annot
*.dep
*.vo
*.vd
*.glob
.*.aux
*.elc
*.summary
\#*\#

# /
/config.status
/config.log
/autom4te.cache
/Makefile
/configure
/install-sh
/semantic.cache
/TAGS
/output_why3
/output_coq
/dep.pdf
/distrib
/why3regtests.err
/why3regtests.out
/.merlin
/src/jessie/.merlin

# /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/
/bench/ce/*.out

# /bin/
/bin/why3.byte
/bin/why3.opt
/bin/why3
/bin/why3ide.byte
/bin/why3ide.opt
/bin/why3ide
/bin/why3config.byte
/bin/why3config.opt
/bin/why3config
/bin/why3doc.byte
/bin/why3doc.opt
/bin/why3doc
/bin/why3extract.byte
/bin/why3extract.opt
/bin/why3extract
/bin/why3execute.byte
/bin/why3execute.opt
/bin/why3execute
/bin/why3prove.byte
/bin/why3prove.opt
/bin/why3prove
/bin/why3realize.byte
/bin/why3realize.opt
/bin/why3realize
/bin/why3replay.byte
/bin/why3replay.opt
/bin/why3replay
/bin/why3session.opt
/bin/why3session.byte
/bin/why3session
/bin/why3shell.opt
/bin/why3shell.byte
/bin/why3shell
/bin/why3wc.opt
/bin/why3wc.byte
/bin/why3wc
/bin/why3webserver.opt
/bin/why3webserver.byte
/bin/why3webserver

# /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/manual.image.out
/doc/manual.synctex.gz
/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/
/doc/texput.log
/doc/extract_ocaml_code
/doc/logic_*.ml
/doc/call_provers_*.ml
/doc/whyconf_*.ml
/doc/*__*.ml

# /lib
/lib/why3-cpulimit
/lib/why3-cpulimit.exe
/lib/why3cpulimit
/lib/why3cpulimit.exe
/lib/why3server
/lib/why3server.exe

# /lib/why3/
/lib/why3/META

# /lib/ocaml/
/lib/ocaml/why3__BigInt_compat.ml

# /share/
/share/emacs/semantic.cache
/share/Makefile.config
/share/drivers
/share/stdlib

# /src/
/src/config.sh

# Coq
/lib/coq/version

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

# Isabelle
/lib/isabelle/bool/
/lib/isabelle/int/
/lib/isabelle/number/
/lib/isabelle/list/
/lib/isabelle/map/
/lib/isabelle/real/
/lib/isabelle/set/
/lib/isabelle/ROOT
/lib/isabelle/Why3_BV.thy
/lib/isabelle/Why3_Number.thy
/lib/isabelle/Why3_Real.thy
/lib/isabelle/Why3_Set.thy
/lib/isabelle/why3.ML
/lib/isabelle/last_build
/lib/isabelle/bv

# /src/driver/
/src/driver/driver_lexer.ml
/src/driver/driver_parser.ml
/src/driver/driver_parser.mli
/src/driver/driver_parser.conflicts
/src/driver/parse_smtv2_model_lexer.ml
/src/driver/parse_smtv2_model_parser.ml
/src/driver/parse_smtv2_model_parser.mli

# /src/parser/
/src/parser/lexer.ml
/src/parser/parser.ml
/src/parser/parser.mli
/src/parser/parser.conflicts
/src/parser/handcrafted.messages.temp
/src/parser/parser_messages.ml

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

# /src/util/
/src/util/config.ml
/src/util/lexlib.ml
/src/util/rc.ml
/src/util/json_lexer.ml
/src/util/json_parser.mli
/src/util/json_parser.ml

# /src/session
/src/session/xml.ml
/src/session/compress.ml
/src/session/strategy_parser.ml

# /src/tools
/src/tools/why3wc.ml

# /src/ide
/src/ide/why3_js.byte
/src/ide/why3_js.js

# /plugins/tptp/
/plugins/tptp/tptp_lexer.ml
/plugins/tptp/tptp_parser.ml
/plugins/tptp/tptp_parser.mli
/plugins/tptp/tptp_parser.conflicts
/plugins/parser/dimacs.ml

# /plugins/python/
/plugins/python/py_lexer.ml
/plugins/python/py_parser.ml
/plugins/python/py_parser.mli
/plugins/python/test/
/plugins/python/py_parser.conflicts

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

# /tests/
/tests/test-jcf/
/tests/test-pgm-jcf/
/tests/test-claude/
/tests/test-and/
/tests/test-extraction/*
!/tests/test-extraction/main.ml
/tests/python/*/why3session.xml
/tests/python/*/why3shapes.gz

# /examples/
/examples/in_progress/course/
/examples/in_progress/wcet_hull/
/examples/in_progress/binary_search2/
/examples/in_progress/binary_search_c/
/examples/in_progress/vacid_0_red_black_trees_harness/
/examples/why3bench.html
/examples/why3regtests.err
/examples/why3regtests.out
/examples/*/*.opt
/examples/*/*.byte
/examples/in_progress/*/*.opt
/examples/in_progress/*/*.byte
/examples/*.html
/examples/*/*.html
!/examples/*/index.html
/examples/*/*/*.html
!/examples/*/*/index.html
/examples/*/*/*/*.html
!/examples/*/*/*/index.html
/examples/style.css
/examples/*/style.css
/examples/*/*/style.css
/examples/*/*/*/style.css
/examples/*/*.tex
/examples/*/*/*.tex
/examples/*/*/*/*.tex
/examples/use_api/runstrat/makejob.opt
/examples/use_api/runstrat/runstrat.opt
/examples/vstte10_max_sum/vstte10_max_sum.ml
/examples/euler001/euler001.ml
/examples/sudoku/sudoku.ml
/examples/sudoku/jsmain.js
/examples/in_progress/sudoku_reloaded/*__*.ml
/examples/in_progress/sudoku_reloaded/jsmain.js
/examples/gcd/euclideanAlgorithm63.ml
/examples/gcd/jsmain.js
/examples/defunctionalization/defunctionalization.ml
/examples/vstte12_combinators/jsmain.js
/examples/vstte12_combinators/vstte12_combinators.ml
/examples/in_progress/bigInt/jsmain.js
/examples/in_progress/bigInt/*__*.ml
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
/examples/prover/.depend
/examples/prover/prover
/examples/prover/prover.ml
/examples/prover/bench/*/*.out
/examples/prover/bench/*/*.txt
/examples/prover/bench1
/examples/prover/bench2
/examples/prover/macro_generator/depend
/examples/prover/macro_generator/build
/examples/in_progress/multiprecision/build/

# Try Why3
/src/trywhy3/trywhy3.byte
/src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.map
/src/trywhy3/alt_ergo_worker.byte
/src/trywhy3/alt_ergo_worker.js
/src/trywhy3/alt_ergo_worker.map
/src/trywhy3/why3_worker.byte
/src/trywhy3/why3_worker.js
/src/trywhy3/why3_worker.map
/src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/index.html
/src/trywhy3/ace-builds/
/src/trywhy3/*.png
/src/trywhy3/alt-ergo*
/src/trywhy3/fontawesome/

# IDE
/src/ide/fontawesome
/src/ide/ace-builds

# jessie3
/src/jessie/config.log
/src/jessie/Makefile
/src/jessie/literals.ml
/src/jessie/tests/ptests_config
/src/jessie/tests/basic/result/*.log
/src/jessie/tests/demo/result/*.log

/trash
trywhy3.tar.gz