From cfdef48659770520b7a0a9a72e468d0621b38a29 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 14:31:48 +0100
Subject: [PATCH] Remove some unnecessary Implicit Types.

These are no longer needed, since fill is no longer a type class.
---
 barrier/heap_lang.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 9e1d83715..aca91e51b 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -108,9 +108,6 @@ Inductive ectx_item :=
 
 Notation ectx := (list ectx_item).
 
-Implicit Types Ki : ectx_item.
-Implicit Types K : ectx.
-
 Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
   | AppLCtx e2 => App e e2
@@ -195,7 +192,7 @@ Definition atomic (e: expr) :=
 We could potentially make this a generic construction. *)
 Inductive prim_step
     (e1 : expr) (σ1 : state) (e2 : expr) (σ2: state) (ef: option expr) : Prop :=
-  Ectx_step (K : ectx) e1' e2' :
+  Ectx_step K e1' e2' :
     e1 = fill K e1' → e2 = fill K e2' →
     head_step e1' σ1 e2' σ2 ef → prim_step e1 σ1 e2 σ2 ef.
 
-- 
GitLab