@@ -805,10 +805,10 @@ elab ist info emode opts fn tm
805805 Just b ->
806806 case unApply (binderTy b) of
807807 (P _ c _, args) ->
808− case lookupCtxt c (idris_classes ist) of
809− [] -> return ()
810− _ -> -- type class, set as injective
811− do mapM_ setinjArg args
808+ case lookupCtxtExact c (idris_classes ist) of
809+ Nothing -> return ()
810+ Just ci -> -- type class, set as injective
811+ do mapM_ setinjArg (getDets 0 (class_determiners ci) args)
812812 -- maybe we can solve more things now...
813813 ulog <- getUnifyLog
814814 probs <- get_probs
@@ -821,6 +821,10 @@ elab ist info emode opts fn tm
821821 setinjArg (P _ n _) = setinj n
822822 setinjArg _ = return ()
823823
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
827+
824828 tacTm (PTactics _) = True
825829 tacTm (PProof _) = True
826830 tacTm _ = False