Convertability for hComp

diff --git a/Eval.hs b/Eval.hs
index 66c7778a79e0d0ba1133715fe9fd98b474fb2b8e..4f28dbfdc637890d134e8749aad82b5f9d24a9bd 100644 (file)
--- 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'