- let _, name, goal, args =
- match patterns with
- | [p] -> p
- | [] ->
+ match patterns with
+ | [_, name, goal, args] ->
+ run_goal env loc name args goal
+
+ | [] ->
+ (* There's no matching goal, but we don't need one if
+ * the tactic doesn't need to be rebuilt.
+ *)
+ let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in
+ let p = Ast.PTactic (loc, tactic, targs) in
+ if needs_rebuild env loc [] p then (