projects
/
cubicaltt.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
098d76f
)
Add the missing line in comp!
author
Anders Mörtberg
<andersmortberg@gmail.com>
Fri, 4 Dec 2015 19:01:46 +0000
(14:01 -0500)
committer
Anders Mörtberg
<andersmortberg@gmail.com>
Fri, 4 Dec 2015 19:01:46 +0000
(14:01 -0500)
Eval.hs
patch
|
blob
|
blame
|
history
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