Interface change: the get_as_string and set_term methods of the term-editors

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

diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml
index 5392fae858729a9b3f6ce711728f927c16c7b054..753f3fc787e89d8cdc3690de376700ef16fb8c68 100644 (file)
--- 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