* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Hbugs_types;;
open Printf;;
let rec string_of_hint = function
- | Use_ring_Luke -> "Use Ring, Luke!"
- | Use_fourier_Luke -> "Use Fourier, Luke!"
- | Use_reflexivity_Luke -> "Use reflexivity, Luke!"
- | Use_symmetry_Luke -> "Use symmetry, Luke!"
- | Use_assumption_Luke -> "Use assumption, Luke!"
- | Use_contradiction_Luke -> "Use contradiction, Luke!"
- | Use_exists_Luke -> "Use exists, Luke!"
- | Use_split_Luke -> "Use split, Luke!"
- | Use_left_Luke -> "Use left, Luke!"
- | Use_right_Luke -> "Use right, Luke!"
- | Use_apply_Luke term -> sprintf "Apply %s, Luke!" term
+ | Use_ring -> "Use Ring, Luke!"
+ | Use_fourier -> "Use Fourier, Luke!"
+ | Use_reflexivity -> "Use reflexivity, Luke!"
+ | Use_symmetry -> "Use symmetry, Luke!"
+ | Use_assumption -> "Use assumption, Luke!"
+ | Use_contradiction -> "Use contradiction, Luke!"
+ | Use_exists -> "Use exists, Luke!"
+ | Use_split -> "Use split, Luke!"
+ | Use_left -> "Use left, Luke!"
+ | Use_right -> "Use right, Luke!"
+ | Use_apply term -> sprintf "Apply %s, Luke!" term
| Hints hints -> String.concat "; " (List.map string_of_hint hints)
;;