Merge PR#314: Miscellaneous fixes for Ocaml warnings.

3 files changed, 10 insertions, 27 deletions

diff --git a/lib/unicode.ml b/lib/unicode.ml
index ced5e258c..959ccaf73 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -124,27 +124,11 @@ exception End_of_input
 let utf8_of_unicode n =
   if n < 128 then
     String.make 1 (Char.chr n)
-  else if n < 2048 then
-    let s = String.make 2 (Char.chr (128 + n mod 64)) in
-    begin
-      s.[0] <- Char.chr (192 + n / 64);
-      s
-    end
-  else if n < 65536 then
-    let s = String.make 3 (Char.chr (128 + n mod 64)) in
-    begin
-      s.[1] <- Char.chr (128 + (n / 64) mod 64);
-      s.[0] <- Char.chr (224 + n / 4096);
-      s
-    end
   else
-    let s = String.make 4 (Char.chr (128 + n mod 64)) in
-    begin
-      s.[2] <- Char.chr (128 + (n / 64) mod 64);
-      s.[1] <- Char.chr (128 + (n / 4096) mod 64);
-      s.[0] <- Char.chr (240 + n / 262144);
-      s
-    end
+    let (m,s) = if n < 2048 then (2,192) else if n < 65536 then (3,224) else (4,240) in
+    String.init m (fun i ->
+        let j = (n lsr ((m - 1 - i) * 6)) land 63 in
+        Char.chr (j + if i = 0 then s else 128))
 
 (* If [s] is some UTF-8 encoded string
    and [i] is a position of some UTF-8 character within [s]
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index b1a6fa63d..fccee6e40 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -1243,11 +1243,10 @@ let declare_extra_genarg_pprule wit
   (f : 'a raw_extra_genarg_printer)
   (g : 'b glob_extra_genarg_printer)
   (h : 'c extra_genarg_printer) =
-  let s = match wit with
-    | ExtraArg s -> ArgT.repr s
-    | _ -> error
-      "Can declare a pretty-printing rule only for extra argument types."
-  in
+  begin match wit with
+    | ExtraArg s -> ()
+    | _          -> error "Can declare a pretty-printing rule only for extra argument types."
+  end;
   let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
   let g x =
     let env = Global.env () in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 0e72a044c..c1a659c38 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -105,7 +105,7 @@ let verbose_phrase verbch loc =
   match verbch with
     | Some ch ->
 	let len = snd loc - fst loc in
-	let s = String.create len in
+	let s = Bytes.create len in
         seek_in ch (fst loc);
         really_input ch s 0 len;
         Feedback.msg_notice (str s)
@@ -162,7 +162,7 @@ let pr_new_syntax po loc chan_beautify ocom =
 let pp_cmd_header loc com =
   let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
   let noblank s =
-    for i = 0 to String.length s - 1 do
+    for i = 0 to Bytes.length s - 1 do
       match s.[i] with
 	| ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~'
 	| _ -> ()