From: Simon Huber <hubsim@gmail.com>
Date: Mon, 8 Jun 2015 10:04:32 +0000 (+0200)
Subject: Convertability for hComp
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=69cf6d0be617caaa2e29f56d4d5b31be5e912028;p=cubicaltt.git

Convertability for hComp
---

diff --git a/Eval.hs b/Eval.hs
index 66c7778..4f28dbf 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -621,6 +621,7 @@ instance Convertible Val where
       (p,VPath i' a')            -> conv ns (p @@ j) (a' `swap` (i',j))
       (VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x')
       (VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts')
+      (VHComp a u ts,VHComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts')
       (VGlue v hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos')
       (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us')
       (VUnGlueElem u _ _,VUnGlueElem u' _ _) -> conv ns u u'