Reintroduce glueElem

diff --git a/Exp.cf b/Exp.cf
index b0f94700081559ff0ab032fadcf78cc5f9419e07..83d9a9951f492586457622134d124a5911160939 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -34,7 +34,7 @@ IdP.          Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
 Comp.         Exp3 ::= "comp" Exp4 Exp4 System ;
 Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "glue" Exp4 System ;
--- GlueElem.     Exp3 ::= "glueElem" Exp4 System ;
+GlueElem.     Exp3 ::= "glueElem" Exp4 System ;
 -- CompElem.     Exp3 ::= "compElem" Exp4 System Exp4 System ;
 -- GlueLine.     Exp3 ::= "glueLine" Formula Formula Exp4 ;
 -- GlueLineElem. Exp3 ::= "glueLineElem" Formula Formula Exp4 ;

diff --git a/Resolver.hs b/Resolver.hs
index 96ddc4d3b8336436fb6acb8f732128d1409e8f1f..68fbb8e83b79bc096c77403803e651358a7d025a 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -202,11 +202,11 @@ resolveExp e = case e of
         CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs
                               <*> mapM resolveFormula phis
       _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi
-  IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
-  Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
-  Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
-  Glue u ts   -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
-  -- GlueElem u ts      -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
+  IdP x y z     -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
+  Comp u v ts   -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+  Fill u v ts   -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+  Glue u ts     -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
+  GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
   -- GlueLine phi psi u ->
   --   CTT.GlueLine <$> resolveExp u <*> resolveFormula phi <*> resolveFormula psi
   -- GlueLineElem phi psi u ->