@@ -670,6 +670,7 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++
670670 getName :: PDecl -> Maybe Name
671671 getName (PTy docs argdocs syn fc opts name ty) = Just name
672672 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)
673+ getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)
673674 getName _ = Nothing
674675 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes
675676 getClauseName (PClause fc name whole with rhs whereBlock) = name
@@ -685,6 +686,8 @@ process h fn (NewDefn decls) = logLvl 3 ("Defining names using these decls: " ++
685686 let tm' = force (normaliseAll ctxt [] tm)
686687 let ty' = force (normaliseAll ctxt [] ty)
687688 updateContext (addCtxtDef (getClauseName clause) (Function ty' tm'))
689+ defineName [PData doc argdocs syn fc opts decl] = do
690+ elabData toplevel syn doc argdocs fc opts decl
688691 getClauses (PClauses fc opts name clauses) = clauses
689692 getClauses _ = []
690693 getRHS :: PClause -> PTerm