From 0ca1717a3a1243d3fd905bb2f6c3d427f1f98dc6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 10 Oct 2016 17:09:24 +0200
Subject: [misc] Remove unused binding.

---
 ltac/pptactic.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index b1a6fa63d6..fccee6e40a 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
-- 
cgit v1.2.3


From 2a4f21db56400ee8928f33c3b47edfee54579afc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 10 Oct 2016 17:10:23 +0200
Subject: [safe-string] Use `String.init` to build string.

---
 lib/unicode.ml | 39 +++++++++++++++++++++------------------
 1 file changed, 21 insertions(+), 18 deletions(-)

diff --git a/lib/unicode.ml b/lib/unicode.ml
index ced5e258c2..3ac4e8ca7c 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -125,26 +125,29 @@ 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
+    String.init 2 (fun idx ->
+        match idx with
+        | 0 -> Char.chr (192 + n / 64)
+        | 1 -> Char.chr (128 + n mod 64)
+        | _ -> 'x'
+      )
   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
+    String.init 3 (fun idx ->
+        match idx with
+        | 0 -> Char.chr (224 + n / 4096)
+        | 1 -> Char.chr (128 + (n / 64) mod 64)
+        | 2 -> Char.chr (128 + n mod 64)
+        | _ -> 'x'
+      )
   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
+    String.init 4 (fun idx ->
+        match idx with
+        | 0 -> Char.chr (240 + n / 262144)
+        | 1 -> Char.chr (128 + (n / 4096) mod 64)
+        | 2 -> Char.chr (128 + (n / 64) mod 64)
+        | 4 -> Char.chr (128 + n mod 64)
+        | _ -> 'x'
+      )
 
 (* If [s] is some UTF-8 encoded string
    and [i] is a position of some UTF-8 character within [s]
-- 
cgit v1.2.3


From a92492652c146c4c51a94922345ddf4c168cdcf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 10 Oct 2016 17:10:48 +0200
Subject: [safe-string] Switch to buffer to `Bytes`

---
 toplevel/vernac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 0e72a044c1..c1a659c38d 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] <- '~'
 	| _ -> ()
-- 
cgit v1.2.3


From 3cdcad29ee9d28b0cb39740004da90a0fe291543 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 30 Jan 2017 15:28:01 +0100
Subject: [unicode] Address comments in PR#314.

---
 lib/unicode.ml | 27 ++++-----------------------
 1 file changed, 4 insertions(+), 23 deletions(-)

diff --git a/lib/unicode.ml b/lib/unicode.ml
index 3ac4e8ca7c..959ccaf73c 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -124,30 +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
-    String.init 2 (fun idx ->
-        match idx with
-        | 0 -> Char.chr (192 + n / 64)
-        | 1 -> Char.chr (128 + n mod 64)
-        | _ -> 'x'
-      )
-  else if n < 65536 then
-    String.init 3 (fun idx ->
-        match idx with
-        | 0 -> Char.chr (224 + n / 4096)
-        | 1 -> Char.chr (128 + (n / 64) mod 64)
-        | 2 -> Char.chr (128 + n mod 64)
-        | _ -> 'x'
-      )
   else
-    String.init 4 (fun idx ->
-        match idx with
-        | 0 -> Char.chr (240 + n / 262144)
-        | 1 -> Char.chr (128 + (n / 4096) mod 64)
-        | 2 -> Char.chr (128 + (n / 64) mod 64)
-        | 4 -> Char.chr (128 + n mod 64)
-        | _ -> 'x'
-      )
+    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]
-- 
cgit v1.2.3