Add more program structure to normal forms.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/Obs/Typing/Context.idr b/src/Obs/Typing/Context.idr
index 4706dca..ad1d0a7 100644
--- a/src/Obs/Typing/Context.idr
+++ b/src/Obs/Typing/Context.idr
@@ -64,7 +64,7 @@ fromVar var = MkDefinition
   { name = var.name
   , sort = var.sort
   , ty = weaken [relevance var.sort] var.ty
-  , tm = point (var.name, (var.sort ** Refl)) Here
+  , tm = point (Just var.name) Here
   , correct = Refl
   }
 
@@ -104,5 +104,5 @@ reduce : (tyCtx : TyContext ctx) -> Map ctx (LogNormalForm ann) (freeVars tyCtx)
 reduce [] = absurd
 reduce (ctx :< def) = add (LogNormalForm ann) (subst def.tm (reduce ctx)) (reduce ctx)
 reduce (ctx ::< var) = add (LogNormalForm ann)
-  (pure $ point (var.name, (var.sort ** Refl)) Here)
+  (pure $ point (Just var.name) Here)
   (\i => pure $ weaken [_] $ !(reduce ctx i))