Merge branch 'callcc-non-cps' of github.com:logsem/gitrees into callc…

…c-non-cps

_CoqProject

@@ -16,7 +16,6 @@ vendor/Binding/Resolver.v
 
 theories/prelude.v
 theories/lang_generic.v
-theories/lang_generic_sem.v
 
 theories/gitree/core.v
 theories/gitree/subofe.v
@@ -30,27 +29,30 @@ theories/gitree.v
 theories/program_logic.v
 
 
-theories/input_lang_delim/lang.v
-theories/input_lang_delim/interp.v
-theories/input_lang_delim/hom.v
-theories/input_lang_delim/logrel.v
+theories/examples/input_lang_delim/lang.v
+theories/examples/input_lang_delim/interp.v
+theories/examples/input_lang_delim/hom.v
+theories/examples/input_lang_delim/logrel.v
 
-theories/input_lang_callcc/lang.v
-theories/input_lang_callcc/interp.v
-theories/input_lang_callcc/hom.v
-theories/input_lang_callcc/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/input_lang/lang.v
-theories/input_lang/interp.v
-theories/input_lang/logpred.v
-theories/input_lang/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/affine_lang/lang.v
-theories/affine_lang/logrel1.v
-theories/affine_lang/logrel2.v
+theories/examples/affine_lang/lang.v
+theories/examples/affine_lang/logrel1.v
+theories/examples/affine_lang/logrel2.v
 
-theories/examples/store.v
-theories/examples/pairs.v
-theories/examples/while.v
-theories/examples/factorial.v
-theories/examples/iter.v
+theories/effects/store.v
+
+theories/lib/pairs.v
+theories/lib/while.v
+theories/lib/factorial.v
+theories/lib/iter.v
+
+theories/utils/finite_sets.v