From 1cdd0df01dd5c802b96c1518361f88eb432f5b7e Mon Sep 17 00:00:00 2001 From: David Raymond Christiansen Date: Fri, 11 Jul 2014 13:57:45 +0200 Subject: [PATCH] Don't do trace when `with` doesn't match This breaks IDESlave support. RE #879 --- src/Idris/ElabDecls.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs index 7603b0679..53d0503e3 100644 --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -1830,7 +1830,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock) logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++ showTmImpls toplhs) case matchClause i toplhs tm of - Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level") + Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level" Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars) lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w