+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
+ in
+ let status, term = select low_status context path term in
+ let _,_,_,subst,_ = status.pstatus in
+ let selections =
+ HExtlib.filter_map
+ (function (i,(Some "expanded",c,_,_)) -> Some i | _ -> None)
+ subst
+ in
+ status, (name, context, term), selections
+;;
+
+let get_goal (status : lowtac_status) (g : int) =