We have a big architectural problem here: the Hbugs hints when applied

[helm.git] / helm / gTopLevel / hbugs.ml

diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml
index 0d71d94e0ddb177c928aedf72a0625a1803c6f8c..b0ad35a7402b7e97a5388066526bdf6013f3148c 100644 (file)
--- 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 () =