+
+(* 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