From 5a0c4eb34708d2c85d91e6cb2c708ed16249e06d Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Wed, 6 Jul 2016 11:29:16 -0400
Subject: stuck trying to figure out dependently typed continuation passing
 style

---
 src/Experiments/DerivationsOptionRectLetInEncoding.v | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'src/Experiments')

diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index c0b6be25b..0f02000d0 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -18,16 +18,6 @@ Local Open Scope equiv_scope.
 Generalizable All Variables.
 
 
-Local Ltac set_evars :=
-  repeat match goal with
-         | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E)
-         end.
-
-Local Ltac subst_evars :=
-  repeat match goal with
-         | [ e := ?E |- _ ] => is_evar E; subst e
-         end.
-
 Definition path_sig {A P} {RA:relation A} {Rsig:relation (@sig A P)}
            {HP:Proper (RA==>Basics.impl) P}
            (H:forall (x y:A) (px:P x) (py:P y), RA x y -> Rsig (exist _ x px) (exist _ y py))
-- 
cgit v1.2.3