From 464439c6e88a35559c7a565819c328b74ef83a09 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jkas@itu.dk>
Date: Tue, 11 Jun 2019 18:55:13 +0200
Subject: [PATCH] Removed involutive file

---
 _CoqProject                  | 1 -
 theories/encodings/stype.v   | 4 ++--
 theories/typing/involutive.v | 4 ----
 theories/typing/stype.v      | 4 +++-
 4 files changed, 5 insertions(+), 8 deletions(-)
 delete mode 100644 theories/typing/involutive.v

diff --git a/_CoqProject b/_CoqProject
index 3a5b644..e859773 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,5 @@
 -Q theories osiris
 -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-theories/typing/involutive.v
 theories/typing/side.v
 theories/typing/stype.v
 theories/encodings/encodable.v
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index fcf0c43..dc38fdd 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -206,7 +206,7 @@ Section stype.
           by iRewrite "Heq" in "Heval".
         - iRewrite "Heq" in "Heval". destruct r as [|vr r]=> //=.
           iSplit; first done.
-          iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive. }
+          iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_stype_involutive. }
       iModIntro. iFrame. auto.
     - iExists _.
       iIntros "{$Hcrf} !>" (v) "HP Hcrf".
@@ -220,7 +220,7 @@ Section stype.
         iDestruct "Hinv'" as "[[-> Heval]|[-> Heval]]".
         - iRewrite "Heq" in "Heval". destruct l as [|vl l]=> //.
           iSplit; first done. simpl.
-          iRewrite "Heval". simpl. iFrame "HP". by rewrite involutive.
+          iRewrite "Heval". simpl. iFrame "HP". by rewrite dual_stype_involutive.
         - iSplit=> //.
           iApply (st_eval_send with "HP").
           by iRewrite "Heq" in "Heval". }
diff --git a/theories/typing/involutive.v b/theories/typing/involutive.v
deleted file mode 100644
index c5d7d9d..0000000
--- a/theories/typing/involutive.v
+++ /dev/null
@@ -1,4 +0,0 @@
-From iris.heap_lang Require Import proofmode notation.
-
-Class Involutive {A} (R : relation A) (f : A → A) :=
-  involutive x : R (f (f x)) x.
\ No newline at end of file
diff --git a/theories/typing/stype.v b/theories/typing/stype.v
index edb21bd..da45f64 100644
--- a/theories/typing/stype.v
+++ b/theories/typing/stype.v
@@ -4,9 +4,11 @@ From stdpp Require Export list.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import updates local_updates.
 From iris.heap_lang Require Import proofmode notation.
-From osiris.typing Require Import involutive.
 Set Default Proof Using "Type".
 
+Class Involutive {A} (R : relation A) (f : A → A) :=
+  involutive x : R (f (f x)) x.
+
 Inductive action := Send | Receive.
 Instance action_inhabited : Inhabited action := populate Send.
 Definition dual_action (a : action) : action :=
-- 
GitLab