From 0ff83361e08eec6d6a5ab9a44f35b0b8590d2031 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Fri, 14 Feb 2014 16:32:20 +0100
Subject: add back original bff function before shape updates

---
 BFFPlug.agda | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/BFFPlug.agda b/BFFPlug.agda
index ef921c2..1d5570c 100644
--- a/BFFPlug.agda
+++ b/BFFPlug.agda
@@ -23,6 +23,9 @@ open DecSetoid A using (Carrier)
 open GetTypes.VecVec public using (Get)
 open BFF.VecBFF A public
 
+bffsameshape : (G : Get) → {n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)
+bffsameshape G {n} = bff G n
+
 bffplug : (G : Get) → (ℕ → ℕ → Maybe ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (∃ λ l → Vec Carrier l)
 bffplug G sput {n} {m} s v with sput n m
 ...                        | nothing = nothing
-- 
cgit v1.2.3