-let select_term low_status (name,context,term) (path, matched) =
- let eq context (status as old_status) t1 t2 =
- let _,_,t2 = relocate t2 context in
- if t2 = t1 then true, status else false, old_status
- in
- let match_term m =
- let rec aux ctx status t =
- let b, status = eq ctx status t m in
- if b then
- let n,h,metasenv,subst,o = status.pstatus in
- let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
- let metasenv, instance, ty =
- NCicMetaSubst.mk_meta ~name:"expanded" metasenv ctx (`WithType ty)
- in
- let metasenv, subst =
- NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx
- t instance
- in
- let status = { status with pstatus = n,h,metasenv,subst,o } in
- status, instance
- else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
- in
- aux
- in
- let rec select status ctx pat cic =
- match pat, cic with
- | NCic.Prod (_,s1,t1), NCic.Prod (n,s2,t2) ->
- let status, s = select status ctx s1 s2 in
- let ctx = (n, NCic.Decl s2) :: ctx in
- let status, t = select status ctx t1 t2 in
- status, NCic.Prod (n,s,t)
- | NCic.Appl l1, NCic.Appl l2 ->
- let status, l =
- List.fold_left2
- (fun (status,l) x y ->
- let status, x = select status ctx x y in
- status, l @ [x])
- (status,[]) l1 l2
- in
- status, NCic.Appl l
- | NCic.Implicit `Hole, t -> status, t
- | NCic.Implicit `Term, t ->
- let status, matched = disambiguate status matched None (Ctx ctx) in
- match_term matched ctx status t
- | _,t -> status, t
+let select_tac ~where ~job move_down_hyps =
+ let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
+ let path =
+ match where with None -> NCic.Implicit `Term | Some where -> where in
+ if not move_down_hyps then
+ select0_tac ~where:(wanted,hyps,Some path) ~job
+ else
+ let path =
+ List.fold_left
+ (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
+ path (List.rev hyps)