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