@@ -976,49 +976,49 @@ TacticSeq ::=
976976-}
977977
978978tactic :: SyntaxInfo -> IdrisParser PTactic
979−tactic syn = do reserved "intro"; ns <- sepBy name (lchar ',')
979+tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (lchar ',')
980980 return $ Intro ns
981981 <|> do reserved "intros"; return Intros
982− <|> try (do reserved "refine"; n <- name
982+ <|> try (do reserved "refine"; n <- (indentPropHolds gtProp *> name)
983983 imps <- some imp
984984 return $ Refine n imps)
985− <|> do reserved "refine"; n <- name
985+ <|> do reserved "refine"; n <- (indentPropHolds gtProp *> name)
986986 i <- get
987987 return $ Refine n []
988− <|> do reserved "mrefine"; n <- name
988+ <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> name)
989989 i <- get
990990 return $ MatchRefine n
991− <|> do reserved "rewrite"; t <- expr syn;
991+ <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
992992 i <- get
993993 return $ Rewrite (desugar syn i t)
994− <|> do reserved "equiv"; t <- expr syn;
994+ <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);
995995 i <- get
996996 return $ Equiv (desugar syn i t)
997− <|> try (do reserved "let"; n <- name; lchar ':';
998− ty <- expr' syn; lchar '='; t <- expr syn;
997+ <|> try (do reserved "let"; n <- (indentPropHolds gtProp *> name); (indentPropHolds gtProp *> lchar ':');
998+ ty <- (indentPropHolds gtProp *> expr' syn); (indentPropHolds gtProp *> lchar '='); t <- (indentPropHolds gtProp *> expr syn);
999999 i <- get
10001000 return $ LetTacTy n (desugar syn i ty) (desugar syn i t))
1001− <|> try (do reserved "let"; n <- name; lchar '=';
1002− t <- expr syn;
1001+ <|> try (do reserved "let"; n <- (indentPropHolds gtProp *> name); (indentPropHolds gtProp *> lchar '=');
1002+ t <- (indentPropHolds gtProp *> expr syn);
10031003 i <- get
10041004 return $ LetTac n (desugar syn i t))
1005− <|> do reserved "focus"; n <- name
1005+ <|> do reserved "focus"; n <- (indentPropHolds gtProp *> name)
10061006 return $ Focus n
1007− <|> do reserved "exact"; t <- expr syn;
1007+ <|> do reserved "exact"; t <- (indentPropHolds gtProp *> expr syn);
10081008 i <- get
10091009 return $ Exact (desugar syn i t)
1010− <|> do reserved "applyTactic"; t <- expr syn;
1010+ <|> do reserved "applyTactic"; t <- (indentPropHolds gtProp *> expr syn);
10111011 i <- get
10121012 return $ ApplyTactic (desugar syn i t)
1013− <|> do reserved "reflect"; t <- expr syn;
1013+ <|> do reserved "reflect"; t <- (indentPropHolds gtProp *> expr syn);
10141014 i <- get
10151015 return $ Reflect (desugar syn i t)
1016− <|> do reserved "fill"; t <- expr syn;
1016+ <|> do reserved "fill"; t <- (indentPropHolds gtProp *> expr syn);
10171017 i <- get
10181018 return $ Fill (desugar syn i t)
1019− <|> do reserved "try"; t <- tactic syn;
1019+ <|> do reserved "try"; t <- (indentPropHolds gtProp *> tactic syn);
10201020 lchar '|';
1021− t1 <- tactic syn
1021+ t1 <- (indentPropHolds gtProp *> tactic syn)
10221022 return $ Try t t1
10231023 <|> do lchar '{'
10241024 t <- tactic syn;