X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fhbugs%2Fhbugs_messages.ml;h=a6aa34b3146688649d9a5c2746588088d625f4fa;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=d792c325004bd0b4ab499dfaf06152092f229e0b;hpb=a21777bd2ac02fd346f168ead468405e4c300855;p=helm.git

diff --git a/helm/ocaml/hbugs/hbugs_messages.ml b/helm/ocaml/hbugs/hbugs_messages.ml
index d792c3250..a6aa34b31 100644
--- a/helm/ocaml/hbugs/hbugs_messages.ml
+++ b/helm/ocaml/hbugs/hbugs_messages.ml
@@ -100,17 +100,17 @@ let parse_state (root: ('a node extension as 'a) node) =
 let parse_hint node =
  let rec parse_hint_node node =
    match node#node_type with
-   | T_element "ring" -> Use_ring_Luke
-   | T_element "fourier" -> Use_fourier_Luke
-   | T_element "reflexivity" -> Use_reflexivity_Luke
-   | T_element "symmetry" -> Use_symmetry_Luke
-   | T_element "assumption" -> Use_assumption_Luke
-   | T_element "contradiction" -> Use_contradiction_Luke
-   | T_element "exists" -> Use_exists_Luke
-   | T_element "split" -> Use_split_Luke
-   | T_element "left" -> Use_left_Luke
-   | T_element "right" -> Use_right_Luke
-   | T_element "apply" -> Use_apply_Luke node#data
+   | T_element "ring" -> Use_ring
+   | T_element "fourier" -> Use_fourier
+   | T_element "reflexivity" -> Use_reflexivity
+   | T_element "symmetry" -> Use_symmetry
+   | T_element "assumption" -> Use_assumption
+   | T_element "contradiction" -> Use_contradiction
+   | T_element "exists" -> Use_exists
+   | T_element "split" -> Use_split
+   | T_element "left" -> Use_left
+   | T_element "right" -> Use_right
+   | T_element "apply" -> Use_apply node#data
    | T_element "hints" ->
        Hints
         (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
@@ -243,17 +243,17 @@ let pp_state = function
   | None -> "<gTopLevelStatus />\n"
 
 let rec pp_hint = function
-  | Use_ring_Luke -> sprintf "<ring />"
-  | Use_fourier_Luke -> sprintf "<fourier />"
-  | Use_reflexivity_Luke -> sprintf "<reflexivity />"
-  | Use_symmetry_Luke -> sprintf "<symmetry />"
-  | Use_assumption_Luke -> sprintf "<assumption />"
-  | Use_contradiction_Luke -> sprintf "<contradiction />"
-  | Use_exists_Luke -> sprintf "<exists />"
-  | Use_split_Luke -> sprintf "<split />"
-  | Use_left_Luke -> sprintf "<left />"
-  | Use_right_Luke -> sprintf "<right />"
-  | Use_apply_Luke term -> sprintf "<apply>%s</apply>" term
+  | Use_ring -> sprintf "<ring />"
+  | Use_fourier -> sprintf "<fourier />"
+  | Use_reflexivity -> sprintf "<reflexivity />"
+  | Use_symmetry -> sprintf "<symmetry />"
+  | Use_assumption -> sprintf "<assumption />"
+  | Use_contradiction -> sprintf "<contradiction />"
+  | Use_exists -> sprintf "<exists />"
+  | Use_split -> sprintf "<split />"
+  | Use_left -> sprintf "<left />"
+  | Use_right -> sprintf "<right />"
+  | Use_apply term -> sprintf "<apply>%s</apply>" term
   | Hints hints ->
       sprintf "<hints>\n%s\n</hints>"
         (String.concat "\n" (List.map pp_hint hints))