@@ -874,12 +874,12 @@ pi syn =
874 symbol "->"
874 symbol "->"
875 sc <- expr syn
875 sc <- expr syn
876 return (bindList (PPi (TacImp [] Dynamic script)) xt sc))
876 return (bindList (PPi (TacImp [] Dynamic script)) xt sc))
877− <|> (if implicitAllowed syn then do
878− xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')
877+ <|> (do xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')
879− symbol "->"
878+ symbol "->"
880− sc <- expr syn
879+ sc <- expr syn
880+ if implicitAllowed syn
881− return (bindList (PPi (Imp opts st False)) xt sc)
881+ then return (bindList (PPi (Imp opts st False)) xt sc)
882− else do fail "no implicit arguments allowed here"))
882+ else fail "no implicit arguments allowed here"))
883 <|> (do x <- opExpr syn
883 <|> (do x <- opExpr syn
884 (do symbol "->"
884 (do symbol "->"
885 sc <- expr syn
885 sc <- expr syn