only parsing warnings left

Author: Kaptch

theories/effects/callcc.v

@@ -41,11 +41,9 @@ Proof.
   repeat f_equiv; apply H0.
 Qed.
 
-Canonical Structure reify_cont : sReifier CtxDep.
-Proof.
-  simple refine {| sReifier_ops := contE;
-                   sReifier_state := unitO
-                |}.
+Program Canonical Structure reify_cont : sReifier CtxDep :=
+  Build_sReifier CtxDep contE unitO _ _ _.
+Next Obligation.
   intros X HX op.
   destruct op as [|[|[]]]; simpl.
   - simple refine (OfeMor (reify_callcc X)).

theories/effects/coroutines.v

@@ -139,9 +139,9 @@ Qed.
 
 Definition CoroutineE : opsInterp := @[CreateE; ResumeE; LabelE; YieldE].
 
-Canonical Structure reify_coroutines : sReifier CtxDep.
-Proof.
-  simple refine {| sReifier_ops := CoroutineE |}.
+Program Canonical Structure reify_coroutines : sReifier CtxDep :=
+  Build_sReifier CtxDep CoroutineE _ _ _ _.
+Next Obligation.
   intros X HX op.
   destruct op as [[]|[[]|[[]|[|[]]]]]; simpl.
   - simple refine (OfeMor (coroutine_create X)).

theories/effects/delim.v

@@ -121,12 +121,9 @@ Section reifiers.
 
 End reifiers.
 
-Canonical Structure reify_delim : sReifier CtxDep.
-Proof.
-  simple refine {|
-             sReifier_ops := delimE;
-             sReifier_state := stateF
-           |}.
+Program Canonical Structure reify_delim : sReifier CtxDep :=
+  Build_sReifier CtxDep delimE stateF _ _ _.
+Next Obligation.
   intros X HX op.
   destruct op as [ | [ | [ | [| []]]]]; simpl.
   - simple refine (OfeMor (reify_shift)).

theories/effects/exceptions.v

@@ -239,12 +239,10 @@ Module Exc (Errors : ExcSig).
           exact (IHσ σ'' Hσ'').
         * rewrite Herr -He. reflexivity.
   Qed.      
-  
-  Canonical Structure reify_exc : sReifier CtxDep.
-  Proof.
-    simple refine {| sReifier_ops := exceptE;
-                      sReifier_state := stateF
-                  |}.
+
+  Program Canonical Structure reify_exc : sReifier CtxDep :=
+    Build_sReifier CtxDep exceptE stateF _ _ _.
+  Next Obligation.
     intros X HX op.
     destruct op as [|[|[|[]]]].
     - simple refine (OfeMor (reify_reg X)).

theories/effects/fork.v

@@ -27,11 +27,9 @@ Proof.
   apply G.
 Qed.
 
-Canonical Structure reify_fork : sReifier NotCtxDep.
-Proof.
-  simple refine {| sReifier_ops := concE;
-                   sReifier_state := stateO
-                |}.
+Program Canonical Structure reify_fork : sReifier NotCtxDep :=
+  Build_sReifier NotCtxDep concE stateO _ _ _.
+Next Obligation.
   intros X HX op.
   destruct op as [? | []]; simpl.
   simple refine (OfeMor (reify_fork' X)).

theories/effects/io_tape.v

@@ -55,11 +55,9 @@ Proof.
   repeat f_equiv; done.
 Qed.
 
-Canonical Structure reify_io : sReifier NotCtxDep.
-Proof.
-  simple refine {| sReifier_ops := ioE;
-                   sReifier_state := stateO
-                |}.
+Program Canonical Structure reify_io : sReifier NotCtxDep :=
+  Build_sReifier NotCtxDep ioE stateO _ _ _.
+Next Obligation.
   intros X HX op.
   destruct op as [[] | [ | []]]; simpl.
   - simple refine (OfeMor (reify_input X)).

theories/effects/store.v

@@ -255,9 +255,9 @@ Program Definition AtomicE : opInterp := {|
 |}.
 
 Definition storeE : opsInterp := @[ReadE;WriteE;AllocE;DeallocE;AtomicE].
-Canonical Structure reify_store : sReifier NotCtxDep.
-Proof.
-  simple refine {| sReifier_ops := storeE |}.
+Program Canonical Structure reify_store : sReifier NotCtxDep :=
+  Build_sReifier NotCtxDep storeE stateF _ _ _.
+Next Obligation.
   intros X HX op.
   destruct op as [[]|[[]|[[]|[|[|[]]]]]]; simpl.
   - simple refine (OfeMor (state_read X)).