(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, []
-;;
+ ;;
+
+ let embed t = fst (embed t) ;;
+
+ let saturate 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, sty
+ ;;
+
+ let is_eq_predicate t = assert false;;
+
end