let atomic_tac htac = distribute_tac (exec htac) ;;
+let try_tac tac status =
+ try
+ tac status
+ with NTacStatus.Error _ ->
+ status
+;;
+
+let first_tac tacl status =
+ let res = HExtlib.list_findopt
+ (fun tac _ ->
+ try Some (tac status) with
+ NTacStatus.Error _ -> None) tacl
+ in
+ match res with
+ | None -> raise (NTacStatus.Error (lazy("No tactic left")))
+ | Some x -> x
+;;
+
let exact_tac t = 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)
;;
+let assumption status goal =
+ let gty = get_goalty status goal in
+ let context = ctx_of gty in
+ let (htac:NTacStatus.tactic) =
+ first_tac (List.map
+ (fun (name,_) ->
+ exact_tac ("",0,(Ast.Ident (name,None))))
+ context)
+ in
+ exec htac status goal
+;;
+
+let assumption_tac =
+ distribute_tac assumption
+;;
+
let find_in_context name context =
let rec aux acc = function
| [] -> raise Not_found
(status, (t,ty) :: l))
(status,[]) l
in
- let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in
- Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;
- status
+ let rdb = status.estatus in
+ let pt, metasenv, subst =
+ Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
+ in
+ let status = { status with pstatus = n,h,metasenv,subst,o } in
+ instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
;;
let auto_tac ~params status =