Fix coq/ltac2#30: Compilation broken since -safe-string PR got merged.

3 files changed, 7 insertions, 6 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 1756e44f76..1489c50c13 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -234,11 +234,11 @@ let () = define2 "ident_equal" ident ident begin fun id1 id2 ->
 end
 
 let () = define1 "ident_to_string" ident begin fun id ->
-  return (Value.of_string (Id.to_string id))
+  return (Value.of_string (Bytes.of_string (Id.to_string id)))
 end
 
 let () = define1 "ident_of_string" string begin fun s ->
-  let id = try Some (Id.of_string s) with _ -> None in
+  let id = try Some (Id.of_string (Bytes.to_string s)) with _ -> None in
   return (Value.of_option Value.of_ident id)
 end
 
@@ -714,6 +714,7 @@ let () = define2 "abstract" (option ident) closure begin fun id f ->
 end
 
 let () = define2 "time" (option string) closure begin fun s f ->
+  let s = Option.map Bytes.to_string s in
   Proofview.tclTIME s (thaw f)
 end
 
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 9f200b439d..9c3b512036 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -74,9 +74,9 @@ val of_char : char -> valexpr
 val to_char : valexpr -> char
 val char : char repr
 
-val of_string : string -> valexpr
-val to_string : valexpr -> string
-val string : string repr
+val of_string : Bytes.t -> valexpr
+val to_string : valexpr -> Bytes.t
+val string : Bytes.t repr
 
 val of_list : ('a -> valexpr) -> 'a list -> valexpr
 val to_list : (valexpr -> 'a) -> valexpr -> 'a list
diff --git a/src/tac2print.ml b/src/tac2print.ml
index 018346ad6a..5f34b54ee6 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -426,7 +426,7 @@ end
 
 let () = register_init "string" begin fun s ->
   let s = to_string s in
-  Pp.quote (Pp.str s)
+  Pp.quote (Pp.str (Bytes.to_string s))
 end
 
 let () = register_init "ident" begin fun id ->