State_change can now contain a state of None indicating that the proof

is completed

diff --git a/helm/hbugs/common/hbugs_types.ml b/helm/hbugs/common/hbugs_types.ml
index 3f5b2f4cb5a4320f029bbe2e676047ba74f277f0..ebfa179941430605e843045ad8761fb79151c798 100644 (file)
--- a/helm/hbugs/common/hbugs_types.ml
+++ b/helm/hbugs/common/hbugs_types.ml
@@ -71,7 +71,7 @@ type message =
   | 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 *)
-  | State_change of client_id * state         (* client_id, new state *)
+  | State_change of client_id * state option  (* client_id, new state *)
   | Wow of client_id                          (* client_id *)
 
   (* tutor -> broker *)