@@ -284,7 +284,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
284284 checkDocs fc argDocs t_in
285285 addDocStr n doc argDocs
286286 addIBC (IBCDoc n)
287− addIBC (IBCOpt n)
288287 let metainf = DataMI params
289288 addIBC (IBCMetaInformation n metainf)
290289 -- TMP HACK! Make this a data option
@@ -293,13 +292,15 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
293292 updateContext (setMetaInformation n metainf)
294293 mapM_ (checkPositive n) cons
295294
295+ -- if there's exactly one constructor, mark both the type and the constructor
296296 case cons of
297297 [(cn,ct)] -> setDetaggable cn >> setDetaggable n
298+ >> addIBC (IBCOpt cn) >> addIBC (IBCOpt n)
298299 _ -> return ()
299300
300− if DefaultEliminator `elem` opts
301− then evalStateT (elabEliminator params n t dcons info) Map.empty
302− else return ()
301+ -- create an eliminator
302+ when (DefaultEliminator `elem` opts) $
303+ evalStateT (elabEliminator params n t dcons info) Map.empty
303304 where
304305 setDetaggable :: Name -> Idris ()
305306 setDetaggable n = do