@@ -98,11 +98,7 @@ elabProvider doc info syn fc what n
98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
99 | ProvPostulate _ <- what ->
99 | ProvPostulate _ <- what ->
100 do -- Add the postulate
100 do -- Add the postulate
101− elabPostulate
101+ elabPostulate info syn doc fc [] n (delab i tm)
103− (fmap (const (Left $ Msg "")) .
104− parseDocstring $ T.pack "Provided postulate")
105− fc [] n (delab i tm)
106 logLvl 3 $ "Elaborated provided postulate " ++ show n
102 logLvl 3 $ "Elaborated provided postulate " ++ show n
107 | otherwise ->
103 | otherwise ->
108 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."