[ fix ] Make Agda compile again.

agda · Oct 14, 2015 · 36a00ac · 36a00ac
1 parent 17ec6dd
commit 36a00ac
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs b/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs
@@ -147,7 +147,7 @@ tellSub i v = do
 tellEq :: Int -> Term -> Term -> NLM ()
 tellEq k u v =
   traceSDocNLM "rewriting" 60 (sep
-               [ text "adding equality between" <+> prettyTCM u <+> "(printed in wrong context)"
+               [ text "adding equality between" <+> prettyTCM u <+> text "(printed in wrong context)"
                , text " and " <+> prettyTCM v
                , text ("(with " ++ show k ++ " free variables)") ]) $ do
   modify $ second $ (PostponedEquation k u v:)