Add the missing line in comp!
authorAnders Mörtberg <andersmortberg@gmail.com>
Fri, 4 Dec 2015 19:01:46 +0000 (14:01 -0500)
committerAnders Mörtberg <andersmortberg@gmail.com>
Fri, 4 Dec 2015 19:01:46 +0000 (14:01 -0500)
Eval.hs

diff --git a/Eval.hs b/Eval.hs
index cee419439509b26d7767fd57ad18ac58106367f4..8616746fafcc2dc3930791fa96131fd9430bb25d 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -285,6 +285,7 @@ comp i a u ts = case a of
   VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts)
   VU -> compUniv u (Map.map (VPath i) ts)
   -- VU    -> glue u (Map.map (eqToIso . VPath i) ts)
+  VCompU a es   -> compU i a es u ts
   VGlue b isos | not (isNeutralGlue i isos u ts) -> compGlue i b isos u ts
   Ter (Sum _ _ nass) env -> case u of
     VCon n us | all isCon (elems ts) -> case lookupLabel n nass of