From da0d6da035206778c1d99ef51f471b4b22016492 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 24 Apr 2017 18:42:03 +0200
Subject: [toplevel] Don't mask critical exceptions in vernac interpretation.

Indeed we were not correctly backtracking in the case of
StackOverflow. It makes sense to remove the inner handler which is a
leftover of a previous attempt, and handle interpretation errors in
load as non-recoverable.

This fixes: https://coq.inria.fr/bugs/show_bug.cgi?id=5485
---
 toplevel/vernac.ml | 40 ++++++++++++++++++----------------------
 1 file changed, 18 insertions(+), 22 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 3359a16721..19753b6f64 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -115,28 +115,23 @@ let rec interp_vernac sid po (loc,com) =
         let f = Loadpath.locate_file fname in
         load_vernac verbosely sid f
     | v ->
-      try
-        let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in
-
-        (* Main STM interaction *)
-        if ntip <> `NewTip then
-          anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
-        (* Due to bug #5363 we cannot use observe here as we should,
-           it otherwise reveals bugs *)
-        (* Stm.observe nsid; *)
-        Stm.finish ();
-
-        (* We could use a more refined criteria that depends on the
-           vernac. For now we imitate the old approach. *)
-        let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
-                         not (Proof_global.there_are_pending_proofs ()) in
-
-        if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
-        nsid
-
-      with exn when CErrors.noncritical exn ->
-        ignore(Stm.edit_at sid);
-        raise exn
+      let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in
+
+      (* Main STM interaction *)
+      if ntip <> `NewTip then
+        anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
+      (* Due to bug #5363 we cannot use observe here as we should,
+         it otherwise reveals bugs *)
+      (* Stm.observe nsid; *)
+      Stm.finish ();
+
+      (* We could use a more refined criteria that depends on the
+         vernac. For now we imitate the old approach. *)
+      let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
+                       not (Proof_global.there_are_pending_proofs ()) in
+
+      if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
+      nsid
   in
     try
       (* The -time option is only supported from console-based
@@ -145,6 +140,7 @@ let rec interp_vernac sid po (loc,com) =
       let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
     with reraise ->
+      ignore(Stm.edit_at sid);
       let (reraise, info) = CErrors.push reraise in
       let loc' = Option.default Loc.ghost (Loc.get_loc info) in
       if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
-- 
cgit v1.2.3


From 0fd7d060e0872a6ae3662dfb7a1fb940b80ef9df Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 24 Apr 2017 19:10:19 +0200
Subject: [toplevel] Don't check proofs in -quick mode.

This fixes a logical error introduced in
ce2b2058587224ade9261cd4127ef4f6e94d356b

Patch by @gares, closes https://coq.inria.fr/bugs/show_bug.cgi?id=5484
---
 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 19753b6f64..f81f77e6ec 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -123,7 +123,9 @@ let rec interp_vernac sid po (loc,com) =
       (* Due to bug #5363 we cannot use observe here as we should,
          it otherwise reveals bugs *)
       (* Stm.observe nsid; *)
-      Stm.finish ();
+
+      let check_proof = Flags.(!compilation_mode = BuildVo || not !batch_mode) in
+      if check_proof then Stm.finish ();
 
       (* We could use a more refined criteria that depends on the
          vernac. For now we imitate the old approach. *)
-- 
cgit v1.2.3


From 4abb41d008fc754f21916dcac9cce49f2d04dd6d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 24 Apr 2017 19:25:48 +0200
Subject: [toplevel] Use exception information for error printing.

This is a partial backtrack on
63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we
disregarded exception and tried to print error messages just by
listening to feedback.

However, feedback error messages are not always emitted due to
https://coq.inria.fr/bugs/show_bug.cgi?id=5479

Thus meanwhile it is safer to go back to printing the information
present in exceptions until we tweak the STM.

This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many
other glitches not reported, such errors in nested proofs.
---
 toplevel/coqloop.ml | 33 +++++++++++++--------------------
 toplevel/coqtop.ml  | 25 ++++++++++---------------
 toplevel/vernac.ml  | 50 +++++++++++++++++++++++++++++++++-----------------
 3 files changed, 56 insertions(+), 52 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4641a2bc86..b608488c8c 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -149,20 +149,6 @@ let valid_buffer_loc ib loc =
   not (Loc.is_ghost loc) &&
   let (b,e) = Loc.unloc loc in b-ib.start >= 0 && e-ib.start < ib.len && b<=e
 
-(* This is specific to the toplevel *)
-let pr_loc loc =
-  if Loc.is_ghost loc then str"<unknown>"
-  else
-    let fname = loc.Loc.fname in
-    if CString.equal fname "" then
-      Loc.(str"Toplevel input, characters " ++ int loc.bp ++
-	   str"-" ++ int loc.ep ++ str":")
-    else
-      Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
-	   str", line " ++ int loc.line_nb ++ str", characters " ++
-	   int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
-	   str":")
-
 (* Toplevel error explanation. *)
 let error_info_for_buffer ?loc buf =
   Option.map (fun loc ->
@@ -177,7 +163,7 @@ let error_info_for_buffer ?loc buf =
           else (mt (), nloc)
           (* we are in batch mode, don't adjust location *)
         else (mt (), loc)
-      in pr_loc loc ++ hl
+      in Topfmt.pr_loc loc ++ hl
     ) loc
 
 (* Actual printing routine *)
@@ -292,6 +278,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
   | FileDependency (_,_) -> ()
   | FileLoaded (_,_) -> ()
   | Custom (_,_,_) -> ()
+  (* Re-enable when we switch back to feedback-based error printing *)
+  | Message (Error,loc,msg) -> ()
+  (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *)
   | Message (lvl,loc,msg) ->
     TopErr.print_error_for_buffer ?loc lvl msg top_buffer
 
@@ -318,11 +307,15 @@ let do_vernac sid =
     | CErrors.Drop ->  (* Last chance *)
         if Mltop.is_ocaml_top() then raise CErrors.Drop
         else (Feedback.msg_error (str "There is no ML toplevel."); sid)
-    (* Exception printing is done now by the feedback listener. *)
-    (* XXX: We need this hack due to the side effects of the exception
-       printer and the reliance of Stm.define on attaching crutial
-       state to exceptions *)
-    | any -> ignore (CErrors.(iprint (push any))); sid
+    (* Exception printing should be done by the feedback listener,
+       however this is not yet ready so we rely on the exception for
+       now. *)
+    | any ->
+      let (e, info) = CErrors.push any in
+      let loc = Loc.get_loc info in
+      let msg = CErrors.iprint (e, info) in
+      TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer;
+      sid
 
 (** Main coq loop : read vernacular expressions until Drop is entered.
     Ctrl-C is handled internally as Sys.Break instead of aborting Coq.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f5f43ff66f..9cf0750654 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -430,10 +430,10 @@ let get_native_name s =
 
 (** Prints info which is either an error or an anomaly and then exits
     with the appropriate error code *)
-let fatal_error info anomaly =
-  let msg = info ++ fnl () in
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg;
-  exit (if anomaly then 129 else 1)
+let fatal_error ?extra exn =
+  Topfmt.print_err_exn ?extra exn;
+  let exit_code = if CErrors.(is_anomaly exn || not (handled exn)) then 129 else 1 in
+  exit exit_code
 
 let parse_args arglist =
   let args = ref arglist in
@@ -596,11 +596,7 @@ let parse_args arglist =
   in
   try
     parse ()
-  with
-    | UserError(_, s) as e ->
-      if ismt s then exit 1
-      else fatal_error (CErrors.print e) false
-    | any -> fatal_error (CErrors.print any) (CErrors.is_anomaly any)
+  with any -> fatal_error any
 
 let init_toplevel arglist =
   init_gc ();
@@ -646,14 +642,13 @@ let init_toplevel arglist =
       check_vio_tasks ();
       outputstate ()
     with any ->
-      let any = CErrors.push any in
       flush_all();
-      let msg =
-        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy) then mt ()
-        else str "Error during initialization: " ++ CErrors.iprint any ++ fnl ()
+      let extra =
+        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
+        then None
+        else Some (str "Error during initialization: ")
       in
-      let is_anomaly e = CErrors.is_anomaly e || not (CErrors.handled e) in
-      fatal_error msg (is_anomaly (fst any))
+      fatal_error ?extra any
   end;
   if !batch_mode then begin
     flush_all();
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f81f77e6ec..8bcf2114b2 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -107,6 +107,16 @@ let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
   with Proof_global.NoCurrentProof -> Pp.str ""
 
+let vernac_error msg =
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" Pp.pp_with msg;
+  flush_all ();
+  exit 1
+
+(* Reenable when we get back to feedback printing *)
+(* let is_end_of_input any = match any with *)
+(*     Stm.End_of_input -> true *)
+(*   | _ -> false *)
+
 let rec interp_vernac sid po (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
@@ -161,17 +171,25 @@ and load_vernac verbosely sid file =
      * raised, which means that we raised the end of the file being loaded *)
     while true do
       let loc, ast =
+          Stm.parse_sentence !rsid in_pa
+        (* If an error in parsing occurs, we propagate the exception
+           so the caller of load_vernac will take care of it. However,
+           in the future it could be possible that we want to handle
+           all the errors as feedback events, thus in this case we
+           should relay the exception here for convenience. A
+           possibility is shown below, however we may want to refactor
+           this code:
+
         try Stm.parse_sentence !rsid in_pa
         with
-        | Stm.End_of_input -> raise Stm.End_of_input
-        | any ->
+        | any when not is_end_of_input any ->
           let (e, info) = CErrors.push any in
           let loc = Loc.get_loc info in
           let msg = CErrors.iprint (e, info) in
           Feedback.msg_error ?loc msg;
           iraise (e, info)
+       *)
       in
-
       (* Printing of vernacs *)
       if !beautify then pr_new_syntax in_pa chan_beautify loc (Some ast);
       Option.iter (vernac_echo loc) in_echo;
@@ -231,13 +249,10 @@ let chop_extension f =
 let ensure_bname src tgt =
   let src, tgt = Filename.basename src, Filename.basename tgt in
   let src, tgt = chop_extension src, chop_extension tgt in
-  if src <> tgt then begin
-    Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
-                        str "Source: " ++ str src                                                ++ fnl () ++
-                        str "Target: " ++ str tgt);
-    flush_all ();
-    exit 1
-  end
+  if src <> tgt then
+    vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
+                  str "Source: " ++ str src                                                ++ fnl () ++
+                  str "Target: " ++ str tgt)
 
 let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
 
@@ -246,17 +261,15 @@ let ensure_vo v vo = ensure ".vo" v vo
 let ensure_vio v vio = ensure ".vio" v vio
 
 let ensure_exists f =
-  if not (Sys.file_exists f) then begin
-    Feedback.msg_error (hov 0 (str "Can't find file" ++ spc () ++ str f));
-    exit 1
-  end
+  if not (Sys.file_exists f) then
+    vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
 (* Compile a vernac file *)
 let compile verbosely f =
   let check_pending_proofs () =
     let pfs = Pfedit.get_all_proof_names () in
-    if not (List.is_empty pfs) then
-      (Feedback.msg_error (str "There are pending proofs"); flush_all (); exit 1) in
+    if not (List.is_empty pfs) then vernac_error (str "There are pending proofs")
+  in
   match !Flags.compilation_mode with
   | BuildVo ->
       let long_f_dot_v = ensure_v f in
@@ -311,5 +324,8 @@ let compile verbosely f =
 
 let compile v f =
   ignore(CoqworkmgrApi.get 1);
-  compile v f;
+  begin
+    try compile v f
+    with any -> Topfmt.print_err_exn any
+  end;
   CoqworkmgrApi.giveback 1
-- 
cgit v1.2.3


From e699313c7a3829016c853b2a1541c2e9151d709c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 25 Apr 2017 18:36:09 +0200
Subject: [toplevel] Remove unused parameter from `Vernac.process_expr`.

---
 toplevel/coqloop.ml |  2 +-
 toplevel/vernac.ml  |  8 ++++----
 toplevel/vernac.mli | 10 +++++++---
 3 files changed, 12 insertions(+), 8 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b608488c8c..9a4f476bd3 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -300,7 +300,7 @@ let do_vernac sid =
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
-    Vernac.process_expr sid top_buffer.tokens (read_sentence sid (fst input))
+    Vernac.process_expr sid (read_sentence sid (fst input))
   with
     | Stm.End_of_input | CErrors.Quit ->
         top_stderr (fnl ()); raise CErrors.Quit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 8bcf2114b2..9ff320ee80 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -117,7 +117,7 @@ let vernac_error msg =
 (*     Stm.End_of_input -> true *)
 (*   | _ -> false *)
 
-let rec interp_vernac sid po (loc,com) =
+let rec interp_vernac sid (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
@@ -195,7 +195,7 @@ and load_vernac verbosely sid file =
       Option.iter (vernac_echo loc) in_echo;
 
       checknav_simple (loc, ast);
-      let nsid = Flags.silently (interp_vernac !rsid in_pa) (loc, ast) in
+      let nsid = Flags.silently (interp_vernac !rsid) (loc, ast) in
       rsid := nsid
     done;
     !rsid
@@ -221,9 +221,9 @@ and load_vernac verbosely sid file =
    of a new state label). An example of state-preserving command is one coming
    from the query panel of Coqide. *)
 
-let process_expr sid po loc_ast =
+let process_expr sid loc_ast =
   checknav_deep loc_ast;
-  interp_vernac sid po loc_ast
+  interp_vernac sid loc_ast
 
 (* XML output hooks *)
 let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index e75f8f9e85..bbc095c687 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -8,11 +8,15 @@
 
 (** Parsing of vernacular. *)
 
-(** Reads and executes vernac commands from a stream. *)
-val process_expr : Stateid.t -> Pcoq.Gram.coq_parsable -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
+(** [process_expr sid cmd] Executes vernac command [cmd]. Callers are
+    expected to handle and print errors in form of exceptions, however
+    care is taken so the state machine is left in a consistent
+    state. *)
+val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
 
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
-    echo the commands if [echo] is set. *)
+    echo the commands if [echo] is set. Callers are expected to handle
+    and print errors in form of exceptions. *)
 val load_vernac : bool -> Stateid.t -> string -> Stateid.t
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)
-- 
cgit v1.2.3


From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 19:36:45 +0200
Subject: Fix omitted labels in function calls

---
 toplevel/coqtop.ml | 4 ++--
 toplevel/vernac.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9cf0750654..c3a7558609 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -292,7 +292,7 @@ let init_gc () =
     between coqtop and coqc. *)
 
 let usage () =
-  Envars.set_coqlib CErrors.error;
+  Envars.set_coqlib ~fail:CErrors.error;
   init_load_path ();
   if !batch_mode then Usage.print_usage_coqc ()
   else begin
@@ -609,7 +609,7 @@ let init_toplevel arglist =
       (* If we have been spawned by the Spawn module, this has to be done
        * early since the master waits us to connect back *)
       Spawned.init_channels ();
-      Envars.set_coqlib CErrors.error;
+      Envars.set_coqlib ~fail:CErrors.error;
       if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
       if !print_config then (Usage.print_config (); exit (exitcode ()));
       if !print_tags then (print_style_tags (); exit (exitcode ()));
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9ff320ee80..48cd70f69d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -125,7 +125,7 @@ let rec interp_vernac sid (loc,com) =
         let f = Loadpath.locate_file fname in
         load_vernac verbosely sid f
     | v ->
-      let nsid, ntip = Stm.add sid (not !Flags.quiet) (loc,v) in
+      let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
 
       (* Main STM interaction *)
       if ntip <> `NewTip then
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 toplevel/vernac.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 48cd70f69d..9f6f77ef1d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -41,7 +41,6 @@ let vernac_echo loc in_chan = let open Loc in
 (* vernac parses the given stream, executes interpfun on the syntax tree it
  * parses, and is verbose on "primitives" commands if verbosely is true *)
 
-let chan_beautify = ref stdout
 let beautify_suffix = ".beautified"
 
 let set_formatter_translator ch =
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 toplevel/coqloop.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 66bbf43f62..13e860a88a 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-
 (** The Coq toplevel loop. *)
 
 (** A buffer for the character read from a channel. We store the command
-- 
cgit v1.2.3


From b20d52da0d040fe37bb75b0b739ad7686f9af127 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 22 Apr 2017 12:55:46 +0200
Subject: Warning 29: non escaped end of line may be non portable

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

(limited to 'toplevel')

diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 66f782ffbe..e457ca61d0 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -83,7 +83,7 @@ let print_usage_channel co command =
 \n  -m, --memory           display total heap size at program exit\
 \n                         (use environment variable\
 \n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
-\n                          for full Gc stats dump)
+\n                          for full Gc stats dump)\
 \n  -native-compiler       precompile files for the native_compute machinery\
 \n  -h, -help, --help      print this list of options\
 \n";
-- 
cgit v1.2.3


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 1fe73e6af81759fa8b78c8660745492ed886d477 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 26 Apr 2017 11:57:58 +0200
Subject: Adding an option "Printing Unfocused".

Off by default.

+ small refactoring of emacs hacks in printer.ml.
---
 toplevel/coqtop.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c3a7558609..5687418f2d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -247,6 +247,7 @@ let set_emacs () =
   if not (Option.is_empty !toploop) then
     error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
+  Printer.enable_goal_tags_printing := true;
   color := `OFF
 
 (** Options for CoqIDE *)
-- 
cgit v1.2.3


From cf0e030f3aebecb316852fc4a152fb212f9e7ef5 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 5 May 2017 15:58:52 +0200
Subject: coqtop -help: don't die if coqlib can't be found

---
 toplevel/coqtop.ml | 10 +++++++++-
 toplevel/usage.ml  |  1 +
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5687418f2d..8f50bfb3d8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -292,9 +292,17 @@ let init_gc () =
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
 
+let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesystem"
+    (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
+
+exception NoCoqLib
 let usage () =
-  Envars.set_coqlib ~fail:CErrors.error;
+  begin
+  try
+  Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib);
   init_load_path ();
+  with NoCoqLib -> usage_no_coqlib ()
+  end;
   if !batch_mode then Usage.print_usage_coqc ()
   else begin
     Mltop.load_ml_objects_raw_rex
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e457ca61d0..e290480354 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -30,6 +30,7 @@ let print_usage_channel co command =
 \n  -R dir coqdir          recursively map physical dir to logical coqdir\
 \n  -Q dir coqdir          map physical dir to logical coqdir\
 \n  -top coqdir            set the toplevel name to be coqdir instead of Top\
+\n  -coqlib dir            set the coq standard library directory\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\
 \n  -noinit                start without loading the Init library\
-- 
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 d411a796341a138cacd72350715871f48f82920b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 5 May 2017 21:31:14 +0200
Subject: [toplevel] Fix a couple of logical errors in error printing.

In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use
exceptions for error printing. However a couple of mistakes were
present in that commit:

- We wrongly absorbed the exception on `Vernac.compile`. However, it
  should be propagated as the caller will correctly print the error
  now. This introduced a critical bug as now `coqc` return the wrong
  exit status on error, breaking all sort of things.

- We printed parsing exceptions twice; now it is not necessary to
  print the exception in the parsing handler as it will be propagated.

I've checked this commit versus all previously reported bugs and it
seems to work; we should definitively add a test-suite case to check
that the exit code of `coqc` is correct, plus several other cases such
as bugs

https://coq.inria.fr/bugs/show_bug.cgi?id=5467
https://coq.inria.fr/bugs/show_bug.cgi?id=5485
https://coq.inria.fr/bugs/show_bug.cgi?id=5484

etc... See also PR #583
---
 toplevel/coqloop.ml | 8 ++++++--
 toplevel/vernac.ml  | 5 +----
 2 files changed, 7 insertions(+), 6 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 9a4f476bd3..a80599cd57 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -173,12 +173,13 @@ let print_error_for_buffer ?loc lvl msg buf =
   then Topfmt.emacs_logger ?pre_hdr lvl msg
   else Topfmt.std_logger   ?pre_hdr lvl msg
 
+(*
 let print_toplevel_parse_error (e, info) buf =
   let loc = Loc.get_loc info in
   let lvl = Feedback.Error in
   let msg = CErrors.iprint (e, info) in
   print_error_for_buffer ?loc lvl msg buf
-
+*)
 end
 
 (*s The Coq prompt is the name of the focused proof, if any, and "Coq"
@@ -260,7 +261,10 @@ let read_sentence sid input =
   with reraise ->
     let reraise = CErrors.push reraise in
     discard_to_dot ();
-    TopErr.print_toplevel_parse_error reraise top_buffer;
+    (* The caller of read_sentence does the error printing now, this
+       should be re-enabled once we rely on the feedback error
+       printer again *)
+    (* TopErr.print_toplevel_parse_error reraise top_buffer; *)
     Exninfo.iraise reraise
 
 (** Coqloop Console feedback handler *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 9f6f77ef1d..4fca4ea184 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -323,8 +323,5 @@ let compile verbosely f =
 
 let compile v f =
   ignore(CoqworkmgrApi.get 1);
-  begin
-    try compile v f
-    with any -> Topfmt.print_err_exn any
-  end;
+  compile v f;
   CoqworkmgrApi.giveback 1
-- 
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


From e6883abb10bd394f3066e6883e563e3bab79fea2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 16 May 2017 18:54:14 +0200
Subject: [toplevel] Restore 8.6 goal printing behavior.

When porting the toplevel to the STM, the logic for goal printing was
simplified too much under optimistic assumptions. The idea was not to
rely on the `vernac_classifier` which is an internal and complicated
beast.

However, it seems there are many cases to consider other than
`is_query`, so at the risk of reimplementing the classifier we revert
to the old approach of using the full classification.

This gives maximum 8.6 compatibility, with the pitfall of having to
call the classifier. Indeed, due to the dynamic nature of the "undo
classifier", we cannot call it after `Stm.add`, as the document tree
will be not the right one, making the classification of undo commands
incorrect (actually raising an error "Cannot undo").
---
 toplevel/vernac.ml | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4fca4ea184..e79ee1a427 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -124,6 +124,16 @@ let rec interp_vernac sid (loc,com) =
         let f = Loadpath.locate_file fname in
         load_vernac verbosely sid f
     | v ->
+
+      (* XXX: We need to run this before add as the classification is
+         highly dynamic and depends on the structure of the
+         document. Hopefully this is fixed when VtBack can be removed
+         and Undo etc... are just interpreted regularly. *)
+      let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
+        | VtProofStep _ | VtStm (VtBack _, _) | VtStartProof _ -> true
+        | _ -> false
+      in
+
       let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in
 
       (* Main STM interaction *)
@@ -137,11 +147,12 @@ let rec interp_vernac sid (loc,com) =
       if check_proof then Stm.finish ();
 
       (* We could use a more refined criteria that depends on the
-         vernac. For now we imitate the old approach. *)
-      let hide_goals = !Flags.batch_mode || is_query v || !Flags.quiet ||
-                       not (Proof_global.there_are_pending_proofs ()) in
+         vernac. For now we imitate the old approach and rely on the
+         classification. *)
+      let print_goals = not !Flags.batch_mode && not !Flags.quiet &&
+                        is_proof_step && Proof_global.there_are_pending_proofs () in
 
-      if not hide_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
+      if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
       nsid
   in
     try
-- 
cgit v1.2.3


From 6ef8a007e77c61d9f8c2b19b19dc22548f1896ca Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 18 May 2017 04:47:38 +0200
Subject: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)

In non-interactive mode, `edit_at` seems to do very weird things, for
instance will try to recompute all the previous states which seems
weird.

We better avoid that to approximate 8.6 behavior while we investigate
more.
---
 toplevel/coqtop.ml | 3 +++
 toplevel/vernac.ml | 4 +++-
 2 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8f50bfb3d8..41d370ea57 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -641,6 +641,9 @@ let init_toplevel arglist =
       init_library_roots ();
       load_vernac_obj ();
       require ();
+      (* XXX: This is incorrect in batch mode, as we will initialize
+         the STM before having done Declaremods.start_library, thus
+         state 1 is invalid. This bug was present in 8.5/8.6. *)
       Stm.init ();
       let sid  = load_rcfile (Stm.get_current_state ()) in
       (* XXX: We ignore this for now, but should be threaded to the toplevels *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index eaf685b184..f8378f8765 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -153,7 +153,9 @@ let rec interp_vernac sid (loc,com) =
       let com = if !Flags.time then VernacTime (loc,com) else com in
       interp com
     with reraise ->
-      ignore(Stm.edit_at sid);
+      (* XXX: In non-interactive mode edit_at seems to do very weird
+         things, so we better avoid it while we investigate *)
+      if not !Flags.batch_mode then ignore(Stm.edit_at sid);
       let (reraise, info) = CErrors.push reraise in
       let loc' = Option.default Loc.ghost (Loc.get_loc info) in
       if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc)
-- 
cgit v1.2.3