From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Tue, 5 Jan 2016 11:50:54 +0000 (+0100)
Subject: use compConstLine
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=1a1e721a3ed584fc1f938482b844714118d4c667;p=cubicaltt.git

use compConstLine
---

diff --git a/Eval.hs b/Eval.hs
index 5ba6899..8605ba9 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -310,6 +310,10 @@ compLine :: Val -> Val -> System Val -> Val
 compLine a u ts = comp i (a @@@ i) u (Map.map (@@@ i) ts)
   where i = fresh (a,u,ts)
 
+compConstLine :: Val -> Val -> System Val -> Val
+compConstLine a u ts = comp i a u (Map.map (@@@ i) ts)
+  where i = fresh (a,u,ts)
+
 comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
 comps i []         _ []         = []
 comps i ((x,a):as) e ((ts,u):tsus) =
@@ -560,7 +564,7 @@ compGlue i a equivs wi0 ws = glueElem vi1' usi1
                  (app (equivContr equivG) (vi1' `face` gamma))
                  (fibsgamma `unionSystem` (fibersys `face` gamma))) equivsI1
 
-        vi1 = compLine (constPath ai1) vi1'
+        vi1 = compConstLine ai1 vi1'
                   (Map.map sndVal fibersys')
 
         usi1 = Map.map fstVal fibersys'
@@ -638,7 +642,7 @@ compU i a eqs wi0 ws = glueElem vi1' usi1
                               (wsi1 `face` gamma) (vsi1 `face` gamma)
             in lemEq eqG (vi1' `face` gamma) (fibsgamma `unionSystem` (fibersys `face` gamma))) eqsI1
 
-        vi1 = compLine (constPath ai1) vi1' (Map.map snd fibersys')
+        vi1 = compConstLine ai1 vi1' (Map.map snd fibersys')
 
         usi1 = Map.map fst fibersys'