X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fhbugs.ml;h=b0ad35a7402b7e97a5388066526bdf6013f3148c;hb=34bdae056b1ac678419cc63437f0c92ee58ef228;hp=0d71d94e0ddb177c928aedf72a0625a1803c6f8c;hpb=7f398a57e81555876212ff38c3c0d1cd821b718f;p=helm.git

diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml
index 0d71d94e0..b0ad35a74 100644
--- a/helm/gTopLevel/hbugs.ml
+++ b/helm/gTopLevel/hbugs.ml
@@ -100,7 +100,14 @@ module Make (Tactics: InvokeTactics.Tactics) : HbugsActions =
       | Use_split_Luke -> Tactics.split ()
       | Use_left_Luke -> Tactics.left ()
       | Use_right_Luke -> Tactics.right ()
-      | Use_apply_Luke term -> Tactics.apply ~term ()
+      | 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 ()
       | Hints _ -> assert false
 
     let rec enable () =