@@ -805,10 +805,10 @@ elab ist info emode opts fn tm
805 Just b ->
805 Just b ->
806 case unApply (binderTy b) of
806 case unApply (binderTy b) of
807 (P _ c _, args) ->
807 (P _ c _, args) ->
808− case lookupCtxt c (idris_classes ist) of
808+ case lookupCtxtExact c (idris_classes ist) of
809− [] -> return ()
809+ Nothing -> return ()
810− _ -> -- type class, set as injective
810+ Just ci -> -- type class, set as injective
811− do mapM_ setinjArg args
811+ do mapM_ setinjArg (getDets 0 (class_determiners ci) args)
812 -- maybe we can solve more things now...
812 -- maybe we can solve more things now...
813 ulog <- getUnifyLog
813 ulog <- getUnifyLog
814 probs <- get_probs
814 probs <- get_probs
@@ -821,6 +821,10 @@ elab ist info emode opts fn tm
821 setinjArg (P _ n _) = setinj n
821 setinjArg (P _ n _) = setinj n
822 setinjArg _ = return ()
822 setinjArg _ = return ()
824+ getDets i ds [] = []
825+ getDets i ds (a : as) | i `elem` ds = a : getDets (i + 1) ds as
826+ | otherwise = getDets (i + 1) ds as
824 tacTm (PTactics _) = True
828 tacTm (PTactics _) = True
825 tacTm (PProof _) = True
829 tacTm (PProof _) = True
826 tacTm _ = False
830 tacTm _ = False