move some stuff to the lib folder

_CoqProject

@@ -27,9 +27,11 @@ theories/proofmode.v
 theories/tests/tp_tests.v
 theories/tests/proofmode_tests.v
 
-theories/examples/lock.v
-theories/examples/counter.v
+theories/lib/lock.v
+theories/lib/counter.v
+theories/lib/Y.v
+
 theories/examples/bit.v
-theories/examples/Y.v
 theories/examples/or.v
 theories/examples/generative.v
+

theories/examples/generative.v

@@ -6,7 +6,7 @@ Those are mostly "generative ADTs". *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Export par.
 From reloc Require Export proofmode prelude.bijections.
-From reloc.examples Require Export counter lock.
+From reloc.lib Require Export counter lock.
 From reloc.typing Require Export interp soundness.
 
 (** Using references for name generation *)

theories/examples/or.v

@@ -79,6 +79,8 @@ Section rules.
       rel_load_r. repeat rel_pure_r. eauto with iFrame.
   Qed.
 
+  Opaque or.
+
   (** Compatibility rule *)
   Lemma or_compatible e1 e2 e1' e2' A :
     (REL e1 << e1' : () → A) -∗
@@ -89,7 +91,6 @@ Section rules.
     rel_bind_l e2. rel_bind_r e2'.
     iApply (refines_bind with "H2").
     iIntros (v2 v2') "#Hv2".
-    (* ^ TODO the arrow interpretation gets unfolded here *)
     rel_bind_l e1. rel_bind_r e1'.
     iApply (refines_bind with "H1").
     iIntros (v1 v1') "#Hv1". iSimpl.

theories/examples/counter.v → theories/lib/counter.v

 From reloc Require Export proofmode.
 From reloc.typing Require Export types interp.
 From reloc.logic Require Import compatibility.
-From reloc.examples Require Import lock.
+From reloc.lib Require Import lock.
 From reloc.typing Require Import soundness.
 
 Definition CG_increment : val := λ: "x" "l",

theories/logic/model.v

@@ -139,7 +139,7 @@ Section semtypes.
 
 End semtypes.
 
-(* Nice notations *)
+(** Nice notations *)
 Notation "()" := lty2_unit : lty_scope.
 Infix "→" := lty2_arr : lty_scope.
 Infix "×" := lty2_prod (at level 80) : lty_scope.
@@ -242,13 +242,6 @@ End related_facts.
 Section monadic.
   Context `{relocG Σ}.
 
-  (* Lemma refines_ret_expr E e1 e2 A : *)
-  (*   interp_expr E e1 e2 A -∗ REL e1 << e2 @ E : A. *)
-  (* Proof. *)
-  (*   iIntros "HA". rewrite refines_eq /refines_def. *)
-  (*   eauto with iFrame. *)
-  (* Qed. *)
-
   Lemma refines_bind K K' E A A' e e' :
     (REL e << e' @ E : A) -∗
     (∀ v v', A v v' -∗

theories/typing/types.v

@@ -2,7 +2,7 @@
 (** (Syntactic) Typing for System F_mu_ref with existential types and concurrency *)
 From stdpp Require Export stringmap.
 From iris.heap_lang Require Export lang notation metatheory.
-From Autosubst Require Import Autosubst.
+From Autosubst Require Export Autosubst.
 
 (** * Types *)
 Inductive type :=