+(****************** smart application ********************)
+
+
+let smart_apply t unit_eq status g =
+ let n,h,metasenv,subst,o = status#obj in
+ let gname, ctx, gty = List.assoc g metasenv in
+ (* let ggty = mk_cic_term context gty in *)
+ let status, t = disambiguate status ctx t None in
+ let status,t = term_of_cic_term status t ctx in
+ let ty = NCicTypeChecker.typeof subst metasenv ctx t in
+ let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in
+ let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ let pterm = if args=[] then t else NCic.Appl(t::args) in
+ let eq_coerc =
+ let uri =
+ NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
+ NCic.Const ref
+ in
+ let smart =
+ NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
+ let smart = mk_cic_term ctx smart in
+ try
+ let status = instantiate status g smart in
+ let _,_,metasenv,subst,_ = status#obj in
+ let _,ctx,jty = List.assoc j metasenv in
+ let jty = NCicUntrusted.apply_subst subst ctx jty in
+ debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
+ fast_eq_check unit_eq status j
+ with
+ | Error _ as e -> debug_print (lazy "error"); raise e
+
+let smart_apply_tac t s =
+ let unit_eq = index_local_equations s#eq_cache s in
+ NTactics.distribute_tac (smart_apply t unit_eq) s
+
+let smart_apply_auto t eq_cache =
+ NTactics.distribute_tac (smart_apply t eq_cache)
+
+