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
+ (new NTacStatus.status low_status#obj stack)#set_pstatus low_status
in
let status = tac status in
- (low_status#set_estatus status)#set_obj status#obj
+ (low_status#set_pstatus status)#set_obj status#obj
;;
let distribute_tac tac (status : #tac_status) =
in
aux s go gc loc_tl
in
- let s0 = (new NTacStatus.status status#obj ())#set_estatus status in
+ let s0 = (new NTacStatus.status status#obj ())#set_pstatus status in
let s0, go0, gc0 = s0, [], [] in
let sn, gon, gcn = aux s0 go0 gc0 g in
debug_print (lazy ("opened: "
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
+ ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn
;;
let atomic_tac htac: #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
let try_tac tac status =
+ let try_tac status =
try
tac status
with NTacStatus.Error _ ->
status
+ in
+ atomic_tac try_tac status
;;
let first_tac tacl status =
let status, instance =
mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
in
- instantiate status goal instance)
+ instantiate ~refine:false status goal instance)
;;
let select_tac ~where ~job move_down_hyps =
rightno: int;
leftno: int;
consno: int;
- lefts: NCic.term list;
- rights: NCic.term list;
reference: NReference.reference;
}
;;
let ref_of_indtyinfo iti = iti.reference;;
let analyze_indty_tac ~what indtyref =
- distribute_tac (fun status goal ->
+ distribute_tac (fun (status as orig_status) goal ->
let goalty = get_goalty status goal in
let status, what = disambiguate status (ctx_of goalty) what None in
let status, ty_what = typeof status (ctx_of what) what in
let leftno = List.length lefts in
let rightno = List.length rights in
indtyref := Some {
- rightno = rightno; leftno = leftno; consno = consno;
- lefts = lefts; rights = rights; reference = r;
+ rightno = rightno; leftno = leftno; consno = consno; reference = r;
};
- exec id_tac status goal)
+ exec id_tac orig_status goal)
;;
let sort_of_goal_tac sortref = distribute_tac (fun status goal ->
`LeftToRight -> "eq" ^ suffix ^ "_r"
| `RightToLeft -> "eq" ^ suffix
in
+ let what = Ast.Appl [what; Ast.Implicit `Vector] in
block_tac
[ select_tac ~where ~job:(`Substexpand 2) true;
exact_tac