From: Simon Huber <hubsim@gmail.com>
Date: Fri, 15 Jan 2016 16:38:32 +0000 (+0100)
Subject: Bugfix in inferType
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=9d386e312035b90452cb08261991107b029cab3c;p=cubicaltt.git

Bugfix in inferType
---

diff --git a/Eval.hs b/Eval.hs
index 20485cb..1c16551 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -256,7 +256,8 @@ inferType v = case v of
     ty         -> error $ "inferType: expected IdP type for " ++ show v
                   ++ ", got " ++ show ty
   VComp a _ _ -> a @@ One
-  VUnGlueElemU _ b es -> compUniv b es
+  VUnGlueElem _ b _  -> b
+  VUnGlueElemU _ b _ -> b
   _ -> error $ "inferType: not neutral " ++ show v
 
 (@@) :: ToFormula a => Val -> a -> Val