Hoist type `pbit` to `language`.

theories/program_logic/language.v

@@ -43,6 +43,8 @@ Class LanguageCtx (Λ : language) (K : expr Λ → expr Λ) := {
 Instance language_ctx_id Λ : LanguageCtx Λ id.
 Proof. constructor; naive_solver. Qed.
 
+Variant pbit := progress | noprogress.
+
 Section language.
   Context {Λ : language}.
   Implicit Types v : val Λ.

theories/program_logic/weakestpre.v

@@ -11,8 +11,6 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
-CoInductive pbit := progress | noprogress.
-
 Definition wp_pre `{irisG Λ Σ} (p : pbit)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
     coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,