@@ -1111,19 +1111,19 @@ tactic :: SyntaxInfo -> IdrisParser PTactic
11111111tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (lchar ',')
11121112 return $ Intro ns
11131113 <|> do reserved "intros"; return Intros
1114− <|> try (do reserved "refine"; n <- (indentPropHolds gtProp *> name)
1114+ <|> try (do reserved "refine"; n <- (indentPropHolds gtProp *> fnName)
11151115 imps <- some imp
11161116 return $ Refine n imps)
1117− <|> do reserved "refine"; n <- (indentPropHolds gtProp *> name)
1117+ <|> do reserved "refine"; n <- (indentPropHolds gtProp *> fnName)
11181118 i <- get
11191119 return $ Refine n []
1120− <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> name)
1120+ <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> fnName)
11211121 i <- get
11221122 return $ MatchRefine n
11231123 <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);
11241124 i <- get
11251125 return $ Rewrite (desugar syn i t)
1126− <|> do reserved "induction"; nm <- (indentPropHolds gtProp *> name);
1126+ <|> do reserved "induction"; nm <- (indentPropHolds gtProp *> fnName);
11271127 return $ Induction nm
11281128 <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);
11291129 i <- get