+let gettactic env loc name =
+ assert (name.[0] = '*');
+ let expr =
+ try Env.find name env
+ with Not_found ->
+ failwithf "%a: tactic ‘%s’ not found" string_loc loc name in
+ let tactic =
+ match expr with
+ | ETactic (loc, tactic) -> tactic
+ | _ ->
+ failwithf "%a: tried to call ‘%s’ which is not a tactic"
+ string_loc loc name in
+ tactic
+