@@ -370,7 +370,8 @@ elab ist info emode opts fn tm
370 elabE (True, a, True, qq) sc
370 elabE (True, a, True, qq) sc
372 elab' ina@(_, a, inty, qq) (PLet n ty val sc)
372 elab' ina@(_, a, inty, qq) (PLet n ty val sc)
373− = do attack;
373+ = do attack
374+ ivs <- get_instances
374 tyn <- getNameFrom (sMN 0 "letty")
375 tyn <- getNameFrom (sMN 0 "letty")
375 claim tyn RType
376 claim tyn RType
376 valn <- getNameFrom (sMN 0 "letval")
377 valn <- getNameFrom (sMN 0 "letval")
@@ -384,6 +385,17 @@ elab ist info emode opts fn tm
384 elabE (True, a, True, qq) ty
385 elabE (True, a, True, qq) ty
385 focus valn
386 focus valn
386 elabE (True, a, True, qq) val
387 elabE (True, a, True, qq) val
388+ ivs' <- get_instances
389+ when (not pattern) $
390+ mapM_ (\n -> do focus n
393+ if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
394+ -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
395+ then try (resolveTC 7 g fn ist)
387 env <- get_env
399 env <- get_env
388 elabE (True, a, inty, qq) sc
400 elabE (True, a, inty, qq) sc
389 -- HACK: If the name leaks into its type, it may leak out of
401 -- HACK: If the name leaks into its type, it may leak out of