From 9b54bda96f51cc5387f195614620fae53dec5bd1 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 3 May 2017 10:47:53 +0200
Subject: FIx bug #5300: uncaught exception in "Print Assumptions".

---
 toplevel/assumptions.ml | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 45c539e229..a865ee987f 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -42,6 +42,11 @@ let rec search_cst_label lab = function
   | (l, SFBconst cb) :: _ when Label.equal l lab -> cb
   | _ :: fields -> search_cst_label lab fields
 
+let rec search_mind_label lab = function
+  | [] -> raise Not_found
+  | (l, SFBmind mind) :: _ when Label.equal l lab -> mind
+  | _ :: fields -> search_mind_label lab fields
+
 (* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But:
     a) I don't see currently what should be used instead
     b) this shouldn't be critical for Print Assumption. At worse some
@@ -133,6 +138,18 @@ let lookup_constant cst =
     else lookup_constant_in_impl cst (Some cb)
   with Not_found -> lookup_constant_in_impl cst None
 
+let lookup_mind_in_impl mind =
+  try
+    let mp,dp,lab = repr_kn (canonical_mind mind) in
+    let fields = memoize_fields_of_mp mp in
+      search_mind_label lab fields
+  with Not_found ->
+    anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind)
+
+let lookup_mind mind =
+  try Global.lookup_mind mind
+  with Not_found -> lookup_mind_in_impl mind
+
 (** Graph traversal of an object, collecting on the way the dependencies of
     traversed objects *)
 
@@ -204,7 +221,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj =
       where I_0, I_1, ... are in the same mutual definition and c_ij
       are all their constructors. *)
    if Refmap_env.mem firstind_ref data then data, ax2ty else
-     let mib = Global.lookup_mind mind in
+     let mib = lookup_mind mind in
      (* Collects references of parameters *)
      let param_ctx = mib.mind_params_ctxt in
      let nparam = List.length param_ctx in
@@ -308,7 +325,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
     else
       accu
   | IndRef (m,_) | ConstructRef ((m,_),_) ->
-      let mind = Global.lookup_mind m in
+      let mind = lookup_mind m in
       if mind.mind_typing_flags.check_guarded then
         accu
       else
-- 
cgit v1.2.3


From 787a2c911b88bff399b37bfa8e11c0f1acecc6cd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 May 2017 08:50:27 +0200
Subject: Fix bug #3659: -time should understand multibyte encodings.

We assume Coq always outputs UTF-8 (is it really the case?) and cut strings
after 30 UTF-8 characters instead of using the standard String function.
---
 toplevel/vernac.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bfdae85d50..2a599444c2 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -160,7 +160,9 @@ let pr_new_syntax po loc chan_beautify ocom =
    and a glimpse of the executed command *)
 
 let pp_cmd_header loc com =
-  let shorten s = try (String.sub s 0 30)^"..." with _ -> s in
+  let shorten s =
+    if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
+  in
   let noblank s =
     for i = 0 to String.length s - 1 do
       match s.[i] with
-- 
cgit v1.2.3


From 684dd06c538ea6024e5dd01bfc6eb416b08ddc14 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 14 May 2017 00:26:16 +0200
Subject: Removing a variable warned unused.

---
 toplevel/metasyntax.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 349c05a38d..0787b058ae 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -520,7 +520,7 @@ let warn_skip_spaces_curly =
       (fun () ->strbrk "Skipping spaces inside curly brackets")
 
 let rec drop_spacing = function
-  | UnpCut _ as u :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt
+  | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt
   | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt
   | fmt -> fmt
 
-- 
cgit v1.2.3