ocaml 3.09 transition

[helm.git] / helm / ocaml / hbugs / hbugs_types.mli

diff --git a/helm/ocaml/hbugs/hbugs_types.mli b/helm/ocaml/hbugs/hbugs_types.mli
index ebfa179941430605e843045ad8761fb79151c798..e3067f2e96cb2168f09667fe59eafc6aefb3580c 100644 (file)
--- 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