From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 5 May 2015 00:10:41 +0000 (+0200)
Subject: Add fix to comp for sums
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7a602002c5a805f98e7586643894fac8f633f9f6;p=cubicaltt.git

Add fix to comp for sums
---

diff --git a/Eval.hs b/Eval.hs
index 3368d1f..7005c93 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -434,6 +434,8 @@ comp i a u ts = case a of
       Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
     VPCon{} -> VComp a u (Map.map (VPath i) ts)
     VComp{} -> VComp a u (Map.map (VPath i) ts)
+    VCompElem _ _ u1 _  -> comp i a u1 ts
+    VElimComp _ _ u1    -> comp i a u1 ts
     _ -> error $ "comp ter sum" ++ show u
 
 compNeg :: Name -> Val -> Val -> System Val -> Val