val refine:
lowtac_status -> NCic.context -> cic_term -> cic_term option ->
lowtac_status * cic_term * cic_term (* status, term, type *)
val refine:
lowtac_status -> NCic.context -> cic_term -> cic_term option ->
lowtac_status * cic_term * cic_term (* status, term, type *)