From e1c839377b2d8f718af4a1fe3164946ab11d03b4 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 12 Mar 2019 15:41:28 +0100
Subject: [PATCH] quickfix

---
 theories/examples/or.v   | 2 +-
 theories/logic/model.v   | 8 ++++----
 theories/typing/interp.v | 5 -----
 3 files changed, 5 insertions(+), 10 deletions(-)

diff --git a/theories/examples/or.v b/theories/examples/or.v
index c7888b3..62112cd 100644
--- a/theories/examples/or.v
+++ b/theories/examples/or.v
@@ -2,7 +2,7 @@
 (** (In)equational theory of erratic choice operator (`or`). *)
 From iris.proofmode Require Import tactics.
 From iris.heap_lang.lib Require Export par.
-From reloc Require Export proofmode examples.Y (* for bot *).
+From reloc Require Export proofmode lib.Y (* for bot *).
 
 (** (Binary) non-determinism can be simluated with concurrency. In
 this file we derive the algebraic laws for parallel "or"/demonic
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 08bad25..0a5a020 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -114,16 +114,16 @@ Section semtypes.
     ∃ A, C A w1 w2)%I.
 
   (** The lty2 constructors are non-expansive *)
-  Instance lty2_prod_ne n : Proper (dist n ==> dist n ==> dist n) lty2_prod.
+  Global Instance lty2_prod_ne n : Proper (dist n ==> dist n ==> dist n) lty2_prod.
   Proof. solve_proper. Qed.
 
-  Instance lty2_sum_ne n : Proper (dist n ==> dist n ==> dist n) lty2_sum.
+  Global Instance lty2_sum_ne n : Proper (dist n ==> dist n ==> dist n) lty2_sum.
   Proof. solve_proper. Qed.
 
-  Instance lty2_arr_ne n : Proper (dist n ==> dist n ==> dist n) lty2_arr.
+  Global Instance lty2_arr_ne n : Proper (dist n ==> dist n ==> dist n) lty2_arr.
   Proof. solve_proper. Qed.
 
-  Instance lty2_rec_ne n : Proper (dist n ==> dist n)
+  Global Instance lty2_rec_ne n : Proper (dist n ==> dist n)
        (lty2_rec : (lty2C Σ -n> lty2C Σ) -> lty2C Σ).
   Proof.
     intros F F' HF.
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index ecce276..1ff154f 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -54,11 +54,6 @@ Section semtypes.
     apply lty2_rec_ne=> X /=.
     apply I. by f_equiv.
   Defined.
-  Next Obligation.
-    intros I τ τ' n Δ Δ' HΔ' ??.
-    rewrite /lty2_forall /lty2_car /=.
-    solve_proper.
-  Defined.
 
   Lemma unboxed_type_sound τ Δ v v' :
     UnboxedType τ →
-- 
GitLab