(rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality)
) status
| _ ->
let arg,dir2,tac,concl_pat,gty =
match hyps_pat with
(rewrite_tac ~direction ~pattern:(None,[],concl_pat) equality)
) status
| _ ->
let arg,dir2,tac,concl_pat,gty =
match hyps_pat with