diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index af3357fe1753d98205ab405938742058a7fc6d6c..c78e841e57f91645411c25784ab8826d3af9b498 100644
--- a/theories/program_logic/language.v
+++ b/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 Λ.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index e81a557af1238fc0e6488167f1fa6f6e9fa2407d..16154c0b56fd9de35d30fe7d4c68c3426ec6a80d 100644
--- a/theories/program_logic/weakestpre.v
+++ b/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 Φ,