[ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
'status * cic_term
-(* default value for refine: false; you can use true if the term has already been refined with
+(* default value for refine: true; you can use false if the term has already been refined with
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