-type hint = string (* TODO consiglio per l'utente *)
-type hint_type = string (* TODO consiglio per l'utente *)
+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 *)
+ (* hints list *)
+ | Hints of hint list
+
+type hint_type = string (* TODO tipo di consiglio per l'utente *)
| Unregister_client of client_id (* client id *)
| List_tutors of client_id (* client_id *)
| Subscribe of client_id * tutor_id list (* client id, tutor id list *)
| Unregister_client of client_id (* client id *)
| List_tutors of client_id (* client_id *)
| Subscribe of client_id * tutor_id list (* client id, tutor id list *)
| Start_musing of broker_id * state (* broker id, state *)
| Abort_musing of broker_id * musing_id (* broker id, musing id *)
| Thanks of broker_id * musing_id (* broker id, musing id *)
| Start_musing of broker_id * state (* broker id, state *)
| Abort_musing of broker_id * musing_id (* broker id, musing id *)
| Thanks of broker_id * musing_id (* broker id, musing id *)