@@ -155,8 +155,16 @@ get_inj = do ES p _ _ <- get
155155 return (injective (fst p))
156156
157157checkInjective :: (Term, Term, Term) -> Elab' aux ()
158−checkInjective (tm, l, r) = if isInjective tm then return ()
158+checkInjective (tm, l, r) = do ctxt <- get_context
159+ if isInj ctxt tm then return ()
159160 else lift $ tfail (NotInjective tm l r)
161+ where isInj ctxt (P _ n _)
162+ | isConName Nothing n ctxt = True
163+ isInj ctxt (App f a) = isInj ctxt f
164+ isInj ctxt (Constant _) = True
165+ isInj ctxt (TType _) = True
166+ isInj ctxt (Bind _ (Pi _) sc) = True
167+ isInj ctxt _ = False
160168
161169-- get instance argument names
162170get_instances :: Elab' aux [Name]