X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fhbugs.ml;h=753f3fc787e89d8cdc3690de376700ef16fb8c68;hb=2afbca45037c56264d1889ced69b5f4844b9ecb9;hp=5392fae858729a9b3f6ce711728f927c16c7b054;hpb=1bfef566743ddd81db375cf66ed3868c5d7df542;p=helm.git

diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml
index 5392fae85..753f3fc78 100644
--- a/helm/gTopLevel/hbugs.ml
+++ b/helm/gTopLevel/hbugs.ml
@@ -124,13 +124,9 @@ module Initialize (Tactics: InvokeTactics.Tactics) : Unit =
       | Use_left_Luke -> Tactics.left ()
       | Use_right_Luke -> Tactics.right ()
       | 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 ()
+         (* we remove the "cic:" prefix *)
+         let term' = String.sub term 4 (String.length term - 4) in
+          Tactics.apply ~term:term' ()
       | Hints _ -> assert false
 
     let _ = use_hint_callback := use_hint