From b3eb5903e672272e696a498c015add360368ff89 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Thu, 9 Nov 2017 11:46:05 +0100
Subject: [PATCH] Hoist type `pbit` to `language`.

---
 theories/program_logic/language.v   | 2 ++
 theories/program_logic/weakestpre.v | 2 --
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index af3357fe1..c78e841e5 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 e81a557af..16154c0b5 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 Φ,
-- 
GitLab