-let change ~where ~with_what status goal =
- let goalty = get_goalty status goal in
- let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
- let path =
- match where with None -> NCic.Implicit `Term | Some where -> where
- in
- let status, newgoalty = assert false (*
- select_term status 1 goalty (wanted,path)*) in
- let status, in_scope, out_scope = reopen status in
- let status = List.fold_left (exact with_what) status in_scope in
-
- let j,(n,cctx,bo,_) = out_scope in
- let _ = typeof status (ctx_of goalty) (Obj.magic (n,cctx,bo)) in
-
- let n,h,metasenv,subst,o = status.pstatus in
- let subst = out_scope :: subst in
- let status = { status with pstatus = n,h,metasenv,subst,o } in
-
- let status, instance =
- mk_meta status (ctx_of newgoalty) (`Decl newgoalty)
- in
- instantiate status goal instance
+let change_tac ~where ~with_what =
+ let change status t =
+ let status, ww = disambiguate status with_what None (ctx_of t) in
+ let status = unify status (ctx_of t) t ww in
+ status, ww
+ in
+ let where = GrafiteDisambiguate.disambiguate_npattern where in
+ select0_tac ~where ~job:(`ChangeWith change)