From: Simon Huber <hubsim@gmail.com>
Date: Thu, 3 Mar 2016 12:38:15 +0000 (+0100)
Subject: Anders bugfix for squeezes
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=09d1d1f710580ea2995ba9061690a176236a5273;p=cubicaltt.git

Anders bugfix for squeezes
---

diff --git a/Eval.hs b/Eval.hs
index 028789b..69deb63 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -386,7 +386,7 @@ squeeze i a u = comp j (a `disj` (i,j)) u $ mkSystem [ (i ~> 1, ui1) ]
 
 squeezes :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val]
 squeezes i xas e us = comps j xas (e `disj` (i,j)) us'
-  where j   = fresh (us,e)
+  where j   = fresh (us,e,Atom i)
         us' = [ (mkSystem [(i ~> 1, u `face` (i ~> 1))],u) | u <- us ]