+ | Use_apply_Luke term ->
+ (* CSC: patch momentanea: la stringa deve essere nel formato *)
+ (* CSC: corretto (ovvero quotata se e' TeX ;-((( *)
+ let term =
+ let term' = String.sub term 4 (String.length term - 4) in
+ "$" ^ Str.global_replace (Str.regexp "_") "\\_" term' ^ "$"
+ in
+ Tactics.apply ~term ()