+let fast_eq_check ~params status goal =
+ let gty = get_goalty status goal in
+ let n,h,metasenv,subst,o = status#obj in
+ let eq_cache = status#eq_cache in
+ let status,t = term_of_cic_term status gty (ctx_of gty) in
+ match
+ NCicParamod.fast_eq_check status metasenv subst (ctx_of gty)
+ eq_cache (NCic.Rel ~-1,t)
+ with
+ | [] -> raise (Error (lazy "no proof found",None))
+ | (pt, metasenv, subst)::_ ->
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ instantiate status goal (mk_cic_term (ctx_of gty) pt)
+;;
+
+let fast_eq_check_tac ~params =
+ NTactics.distribute_tac (fast_eq_check ~params)
+;;
+