- let saturate t ty =
- let sty, _, args =
- (* CSC: NCicPp.status is the best I can put here *)
- (* WR: and I can't guess a user id, so I must put None *)
- NCicMetaSubst.saturate (new NCicPp.status None) ~delta:0 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
- ;;
-