X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fhbugs%2Fhbugs_types.mli;h=e3067f2e96cb2168f09667fe59eafc6aefb3580c;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ebfa179941430605e843045ad8761fb79151c798;hpb=a21777bd2ac02fd346f168ead468405e4c300855;p=helm.git

diff --git a/helm/ocaml/hbugs/hbugs_types.mli b/helm/ocaml/hbugs/hbugs_types.mli
index ebfa17994..e3067f2e9 100644
--- a/helm/ocaml/hbugs/hbugs_types.mli
+++ b/helm/ocaml/hbugs/hbugs_types.mli
@@ -37,17 +37,17 @@ type state =  (* proof assitant's state: proof type, proof body, goal *)
 
 type hint =
     (* tactics usage related hints *)
-  | Use_ring_Luke
-  | Use_fourier_Luke
-  | Use_reflexivity_Luke
-  | Use_symmetry_Luke
-  | Use_assumption_Luke
-  | Use_contradiction_Luke
-  | Use_exists_Luke
-  | Use_split_Luke
-  | Use_left_Luke
-  | Use_right_Luke
-  | Use_apply_Luke of string        (* use apply tactic on embedded term *)
+  | Use_ring
+  | Use_fourier
+  | Use_reflexivity
+  | Use_symmetry
+  | Use_assumption
+  | Use_contradiction
+  | Use_exists
+  | Use_split
+  | Use_left
+  | Use_right
+  | Use_apply of string        (* use apply tactic on embedded term *)
     (* hints list *)
   | Hints of hint list