Stm.get_hint_ctx: remove unused Str.split

With suggest proof using out of the kernel the format of context_used
in .aux is just the list of ids wanted by get_hint_ctx.
(split x s when x doesn't appear in s just returns the singleton list [s])

1 files changed, 6 insertions, 10 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 220ed9be4..26b3320aa 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1145,16 +1145,12 @@ let set_compilation_hints file =
 
 let get_hint_ctx loc =
   let s = Aux_file.get ?loc !hints "context_used" in
-  match Str.split (Str.regexp ";") s with
-  | ids :: _ ->
-      let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
-      let ids = List.map (fun id -> Loc.tag id) ids in
-      begin match ids with
-      | [] -> SsEmpty
-      | x :: xs ->
-          List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
-      end
-  | _ -> raise Not_found
+  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+  let ids = List.map (fun id -> Loc.tag id) ids in
+  match ids with
+  | [] -> SsEmpty
+  | x :: xs ->
+    List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
 
 let get_hint_bp_time proof_name =
   try float_of_string (Aux_file.get !hints proof_name)