- let bag, maxvar = Terms.empty_bag, 0 in
- let (bag,maxvar), passives =
+
+ let rec embed = function
+ | NCic.Meta (i,_) -> Terms.Var i, [i]
+ | NCic.Appl l ->
+ let rec aux acc l = function
+ |[] -> acc@l
+ |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
+ in
+ let res,vars = List.fold_left
+ (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
+ in (Terms.Node (List.rev res)), vars
+ | t -> Terms.Leaf t, []
+ in
+
+ let embed t = fst (embed t) in
+
+ let saturate ~is_goal t ty =
+ let sty, _, args =
+ NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context ty 0
+ in
+ let proof =
+ if args = [] then Terms.Leaf t
+ else Terms.Node (Terms.Leaf t :: List.map embed args)
+ in
+ let sty = embed sty in
+ proof, if is_goal then [sty],[] else [],[sty]
+ in
+ let goal = saturate ~is_goal:true g_t g_ty in
+ let hypotheses = List.map (fun (t,ty) -> saturate ~is_goal:false t ty) table in
+ (*let (bag,maxvar), passives =