@@ -1111,19 +1111,19 @@ tactic :: SyntaxInfo -> IdrisParser PTactic
1111tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (lchar ',')
1111tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (lchar ',')
1112 return $ Intro ns
1112 return $ Intro ns
1113 <|> do reserved "intros"; return Intros
1113 <|> do reserved "intros"; return Intros
1114− <|> try (do reserved "refine"; n <- (indentPropHolds gtProp *> name)
1114+ <|> try (do reserved "refine"; n <- (indentPropHolds gtProp *> fnName)
1115 imps <- some imp
1115 imps <- some imp
1116 return $ Refine n imps)
1116 return $ Refine n imps)
1117− <|> do reserved "refine"; n <- (indentPropHolds gtProp *> name)
1117+ <|> do reserved "refine"; n <- (indentPropHolds gtProp *> fnName)
1118 i <- get
1118 i <- get
1119 return $ Refine n []
1119 return $ Refine n []
1120− <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> name)
1120+ <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> fnName)
1121 i <- get
1121 i <- get
1122 return $ MatchRefine n
1122 return $ MatchRefine n
1123 <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
1123 <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
1124 i <- get
1124 i <- get
1125 return $ Rewrite (desugar syn i t)
1125 return $ Rewrite (desugar syn i t)
1126− <|> do reserved "induction"; nm <- (indentPropHolds gtProp *> name);
1126+ <|> do reserved "induction"; nm <- (indentPropHolds gtProp *> fnName);
1127 return $ Induction nm
1127 return $ Induction nm
1128 <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);
1128 <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);
1129 i <- get
1129 i <- get