@@ -91,8 +91,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params
91 -- if the type is not complete, note that we'll need to infer
91 -- if the type is not complete, note that we'll need to infer
92 -- things later (for solving metavariables)
92 -- things later (for solving metavariables)
93 when (not (null ds)) $ addTyInferred n
93 when (not (null ds)) $ addTyInferred n
94−-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
94+
96 mapM_ (elabCaseBlock info opts) is
95 mapM_ (elabCaseBlock info opts) is
97 ctxt <- getContext
96 ctxt <- getContext
98 logLvl 5 $ "Rechecking"
97 logLvl 5 $ "Rechecking"
@@ -1268,10 +1267,6 @@ checkPossible info fc tcgen fname lhs_in
1268 case recheck ctxt [] (forget lhs_tm) lhs_tm of
1267 case recheck ctxt [] (forget lhs_tm) lhs_tm of
1269 OK _ -> return True
1268 OK _ -> return True
1270 err -> return False
1269 err -> return False
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)
1275 Error err -> if tcgen then return False
1270 Error err -> if tcgen then return False
1276 else return (impossibleError err)
1271 else return (impossibleError err)
1277 where impossibleError (CantUnify _ topx topy e _ _)
1272 where impossibleError (CantUnify _ topx topy e _ _)
@@ -1978,10 +1973,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
1978 iLOG (show idecls)
1973 iLOG (show idecls)
1979 mapM_ (elabDecl EAll info) idecls
1974 mapM_ (elabDecl EAll info) idecls
1980 addIBC (IBCInstance intInst n iname)
1975 addIBC (IBCInstance intInst n iname)
1981−-- -- for each constraint, build a top level function to chase it
1976+
1982−-- logLvl 5 $ "Building functions"
1983−-- fns <- mapM (cfun (instanceName ci) constraint syn idecls) cs
1984−-- mapM_ (elabDecl EAll info) (concat fns)
1986 intInst = case ps of
1978 intInst = case ps of
1987 [PConstant (AType (ATInt ITNative))] -> True
1979 [PConstant (AType (ATInt ITNative))] -> True