@@ -91,8 +91,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
9191 -- if the type is not complete, note that we'll need to infer
9292 -- things later (for solving metavariables)
9393 when (not (null ds)) $ addTyInferred n
94−-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
95−-- addDeferred ds'
94+
9695 mapM_ (elabCaseBlock info opts) is
9796 ctxt <- getContext
9897 logLvl 5 $ "Rechecking"
@@ -1268,10 +1267,6 @@ checkPossible info fc tcgen fname lhs_in
12681267 case recheck ctxt [] (forget lhs_tm) lhs_tm of
12691268 OK _ -> return True
12701269 err -> return False
1271−
1272−-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
1273−-- return (not b) -- then return (Just lhs_tm) else return Nothing
1274−-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
12751270 Error err -> if tcgen then return False
12761271 else return (impossibleError err)
12771272 where impossibleError (CantUnify _ topx topy e _ _)
@@ -1978,10 +1973,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
19781973 iLOG (show idecls)
19791974 mapM_ (elabDecl EAll info) idecls
19801975 addIBC (IBCInstance intInst n iname)
1981−-- -- for each constraint, build a top level function to chase it
1982−-- logLvl 5 $ "Building functions"
1983−-- fns <- mapM (cfun (instanceName ci) constraint syn idecls) cs
1984−-- mapM_ (elabDecl EAll info) (concat fns)
1976+
19851977 where
19861978 intInst = case ps of
19871979 [PConstant (AType (ATInt ITNative))] -> True