Bugfix in inferType

diff --git a/Eval.hs b/Eval.hs
index 20485cbe6cc8787b6d5305285d44fd707121fd9c..1c16551f457745b54d5d3c002e7fde4f382a3aa1 100644 (file)
--- 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