_CoqProject

-Q theories gitrees
-Q vendor/Binding Binding
-arg -w -arg -ssr-search-moved

vendor/Binding/Properties.v
vendor/Binding/Lib.v
vendor/Binding/Set.v
vendor/Binding/Auto.v
vendor/Binding/Core.v
vendor/Binding/Inc.v
vendor/Binding/Intrinsic.v
vendor/Binding/TermSimpl.v
vendor/Binding/Product.v
vendor/Binding/Env.v
vendor/Binding/Resolver.v

theories/prelude.v
theories/lang_generic.v

theories/gitree/core.v
theories/gitree/subofe.v
theories/gitree/lambda.v
theories/gitree/reify.v
theories/gitree/greifiers.v
theories/gitree/reductions.v
theories/gitree/weakestpre.v
theories/hom.v
theories/gitree.v

theories/program_logic.v

theories/effects/store.v
theories/effects/callcc.v
theories/effects/io_tape.v
theories/effects/exceptions.v
theories/effects/delim.v

theories/lib/pairs.v
theories/lib/while.v
theories/lib/factorial.v
theories/lib/iter.v

theories/examples/delim_lang/lang.v
theories/examples/delim_lang/typing.v
theories/examples/delim_lang/interp.v
theories/examples/delim_lang/hom.v
theories/examples/delim_lang/example.v
theories/examples/delim_lang/logpred.v
theories/examples/delim_lang/logrel.v

theories/examples/input_lang_callcc/lang.v
theories/examples/input_lang_callcc/interp.v
theories/examples/input_lang_callcc/hom.v
theories/examples/input_lang_callcc/logrel.v

theories/examples/input_lang/lang.v
theories/examples/input_lang/interp.v
theories/examples/input_lang/logpred.v
theories/examples/input_lang/logrel.v

theories/examples/except_lang/lang.v
theories/examples/except_lang/interp.v
theories/examples/except_lang/typing.v

theories/examples/affine_lang/lang.v
theories/examples/affine_lang/logrel1.v
theories/examples/affine_lang/logrel2.v

theories/utils/finite_sets.v