@@ -177,7 +177,7 @@ data Tactic = Try Tactic Tactic
177 -- ^ focus a named hole
177 -- ^ focus a named hole
178 | Rewrite TT
178 | Rewrite TT
179 -- ^ rewrite using the reflected rep. of a equality proof
179 -- ^ rewrite using the reflected rep. of a equality proof
180− | Induction TT
180+ | Induction TTName
181 -- ^ do induction on the particular expression
181 -- ^ do induction on the particular expression
182 | LetTac TTName TT
182 | LetTac TTName TT
183 -- ^ name a reflected term
183 -- ^ name a reflected term