-let apply t (status as orig,goal) =
- let goal = get_goal status goal in
- let status, t = disambiguate status t goal (Term goal) in
- let subst, metasenv =
- (goal, (name, context, t, gty)):: subst,
- List.filter(fun (x,_) -> x <> goal) metasenv
- in
- return ~orig status
+let instantiate status i t =
+ let name,height,metasenv,subst,obj = status.pstatus in
+ let _, context, ty = List.assoc i metasenv in
+ let _,_,t = relocate t context in
+ let m = NCic.Meta (i,(0,NCic.Irl (List.length context))) in
+ let db = NCicUnifHint.db () in (* XXX fixme *)
+ let metasenv, subst = NCicUnification.unify db metasenv subst context m t in
+ { status with pstatus = (name,height,metasenv,subst,obj) }