X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fhbugs%2Fhbugs_messages.ml;h=4767b2aee4e0ccf73fff36bdf3803a3c164a9fef;hb=489ee5290cce2247291b8c5c53b98d493e7f6b99;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..4767b2aee 100644
--- a/helm/ocaml/hbugs/hbugs_messages.ml
+++ b/helm/ocaml/hbugs/hbugs_messages.ml
@@ -26,6 +26,8 @@
* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_types;;
open Printf;;
open Pxp_document;;
@@ -100,17 +102,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 +245,17 @@ let pp_state = function
| None -> "\n"
let rec pp_hint = function
- | Use_ring_Luke -> sprintf ""
- | Use_fourier_Luke -> sprintf ""
- | Use_reflexivity_Luke -> sprintf ""
- | Use_symmetry_Luke -> sprintf ""
- | Use_assumption_Luke -> sprintf ""
- | Use_contradiction_Luke -> sprintf ""
- | Use_exists_Luke -> sprintf ""
- | Use_split_Luke -> sprintf ""
- | Use_left_Luke -> sprintf ""
- | Use_right_Luke -> sprintf ""
- | Use_apply_Luke term -> sprintf "%s" term
+ | Use_ring -> sprintf ""
+ | Use_fourier -> sprintf ""
+ | Use_reflexivity -> sprintf ""
+ | Use_symmetry -> sprintf ""
+ | Use_assumption -> sprintf ""
+ | Use_contradiction -> sprintf ""
+ | Use_exists -> sprintf ""
+ | Use_split -> sprintf ""
+ | Use_left -> sprintf ""
+ | Use_right -> sprintf ""
+ | Use_apply term -> sprintf "%s" term
| Hints hints ->
sprintf "\n%s\n"
(String.concat "\n" (List.map pp_hint hints))