the expected type for the meta (e.g. after a reduction tactic) *)
val instantiate: #pstatus as 'status -> ?refine:bool -> int -> cic_term -> 'status
val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status
the expected type for the meta (e.g. after a reduction tactic) *)
val instantiate: #pstatus as 'status -> ?refine:bool -> int -> cic_term -> 'status
val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status