(e.g. the tactic could perform a global analysis of the set of goals)
*)
-let exec tac low_status g =
+let exec tac (low_status : #lowtac_status) g =
let stack = [ [0,Open g], [], [], `NoTag ] in
let status =
- (new NTacStatus.status low_status#obj stack)#set_estatus
- (low_status :> NEstatus.status)
+ (new NTacStatus.status low_status#obj stack)#set_estatus low_status
in
let status = tac status in
- (low_status#set_estatus (status :> NEstatus.status))#set_obj status#obj
+ (low_status#set_estatus status)#set_obj status#obj
;;
-let distribute_tac tac status =
+let distribute_tac tac (status : #tac_status) =
match status#stack with
| [] -> assert false
| (g, t, k, tag) :: s ->
let stack =
(zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
in
- ((status#set_stack stack)#set_obj (sn :> lowtac_status)#obj)#set_estatus (sn :> NEstatus.status)
+ ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
;;
let atomic_tac htac = distribute_tac (exec htac) ;;
| Some x -> x
;;
-let exact_tac t = distribute_tac (fun status goal ->
+let exact_tac t : 's tactic = distribute_tac (fun status goal ->
let goalty = get_goalty status goal in
let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
instantiate status goal t)