@@ -1,5 +1,4 @@
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
2−{-# OPTIONS_GHC -O0 #-}
3module Idris.ParseExpr where
2module Idris.ParseExpr where
5import Prelude hiding (pi)
4import Prelude hiding (pi)
@@ -877,7 +876,7 @@ explicitPi opts st syn
878autoImplicit opts st syn
877autoImplicit opts st syn
879 = do reserved "auto"
878 = do reserved "auto"
880− when (st == Static) $ fail "auto type constraints can not be static"
879+ when (st == Static) $ fail "auto implicits can not be static"
881 xt <- typeDeclList syn
880 xt <- typeDeclList syn
882 lchar '}'
881 lchar '}'
883 symbol "->"
882 symbol "->"
@@ -887,7 +886,7 @@ autoImplicit opts st syn
888defaultImplicit opts st syn = do
887defaultImplicit opts st syn = do
889 reserved "default"
888 reserved "default"
890− when (st == Static) $ fail "default tactic constraints can not be static"
889+ when (st == Static) $ fail "default implicits can not be static"
891 ist <- get
890 ist <- get
892 script' <- simpleExpr syn
891 script' <- simpleExpr syn
893 let script = debindApp syn . desugar syn ist $ script'
892 let script = debindApp syn . desugar syn ist $ script'