val metas_of_term : #pstatus as 'status -> cic_term -> int list
val get_goalty: #pstatus -> int -> cic_term
+val get_subst: #pstatus -> NCic.substitution
val mk_meta:
#pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
[ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->