Merge branch 'v8.5'

19 files changed, 218 insertions, 124 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 0fe316b56..fa0adf979 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -460,10 +460,6 @@ let close_coqtop coqtop =
 
 let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop
 
-let break_coqtop coqtop =
-  try !interrupter (CoqTop.unixpid coqtop.handle.proc)
-  with _ -> Minilib.log "Error while sending Ctrl-C"
-
 let get_arguments coqtop = coqtop.sup_args
 
 let set_arguments coqtop args =
@@ -513,6 +509,17 @@ let search flags = eval_call (Xmlprotocol.search flags)
 let init x = eval_call (Xmlprotocol.init x)
 let stop_worker x = eval_call (Xmlprotocol.stop_worker x)
 
+let break_coqtop coqtop workers =
+  if coqtop.status = Busy then
+    try !interrupter (CoqTop.unixpid coqtop.handle.proc)
+    with _ -> Minilib.log "Error while sending Ctrl-C"
+  else
+    let rec aux = function
+    | [] -> Void
+    | w :: ws -> stop_worker w coqtop.handle (fun _ -> aux ws)
+    in
+      let Void = aux workers in ()
+
 module PrintOpt =
 struct
   type t = string list
diff --git a/ide/coq.mli b/ide/coq.mli
index d9eda0f34..7cef6a4d0 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -70,8 +70,8 @@ val init_coqtop : coqtop -> unit task -> unit
 (** Finish initializing a freshly spawned coqtop, by running a first task on it.
     The task should run its inner continuation at the end. *)
 
-val break_coqtop : coqtop -> unit
-(** Interrupt the current computation of coqtop. *)
+val break_coqtop : coqtop -> string list -> unit
+(** Interrupt the current computation of coqtop or the worker if coqtop it not running. *)
 
 val close_coqtop : coqtop -> unit
 (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 9f36c4e36..6200f1490 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -174,6 +174,55 @@ let validate s =
 
 module Doc = Document
 
+let segment_model (doc : sentence Doc.document) : Wg_Segment.model =
+object (self)
+
+  val mutable cbs = []
+
+  val mutable document_length = 0
+
+  method length = document_length
+
+  method changed ~callback = cbs <- callback :: cbs
+
+  method fold : 'a. ('a -> Wg_Segment.color -> 'a) -> 'a -> 'a = fun f accu ->
+    let fold accu _ _ s =
+      let flags = List.map mem_flag_of_flag s.flags in
+      f accu (flags_to_color flags)
+    in
+    Doc.fold_all doc accu fold
+
+  method private on_changed (i, f) =
+    let data = (i, flags_to_color f) in
+    List.iter (fun f -> f (`SET data)) cbs
+
+  method private on_push s ctx =
+    let after = match ctx with
+    | None -> []
+    | Some (l, _) -> l
+    in
+    List.iter (fun s -> set_index s (s.index + 1)) after;
+    set_index s (document_length - List.length after);
+    ignore ((SentenceId.connect s)#changed self#on_changed);
+    document_length <- document_length + 1;
+    List.iter (fun f -> f `INSERT) cbs
+
+  method private on_pop s ctx =
+    let () = match ctx with
+    | None -> ()
+    | Some (l, _) -> List.iter (fun s -> set_index s (s.index - 1)) l
+    in
+    set_index s (-1);
+    document_length <- document_length - 1;
+    List.iter (fun f -> f `REMOVE) cbs
+
+  initializer
+    let _ = (Doc.connect doc)#pushed self#on_push in
+    let _ = (Doc.connect doc)#popped self#on_pop in
+    ()
+
+end
+
 class coqops
   (_script:Wg_ScriptView.script_view)
   (_pv:Wg_ProofView.proof_view)
@@ -206,20 +255,8 @@ object(self)
     script#misc#set_has_tooltip true;
     ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback);
     feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback;
-    let on_changed (i, f) = segment#add i (flags_to_color f) in
-    let on_push s =
-      set_index s document_length;
-      ignore ((SentenceId.connect s)#changed on_changed);
-      document_length <- succ document_length;
-      segment#set_length document_length;
-      let flags = List.map mem_flag_of_flag s.flags in
-      segment#add s.index (flags_to_color flags);
-    in
-    let on_pop s =
-      set_index s (-1);
-      document_length <- pred document_length;
-      segment#set_length document_length;
-    in
+    let md = segment_model document in
+    segment#set_model md;
     let on_click id =
       let find _ _ s = Int.equal s.index id in
       let sentence = Doc.find document find in
@@ -235,8 +272,6 @@ object(self)
       script#buffer#place_cursor iter;
       ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter)
     in
-    let _ = (Doc.connect document)#pushed on_push in
-    let _ = (Doc.connect document)#popped on_pop in
     let _ = segment#connect#clicked on_click in
     ()
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8a952f260..1fe393d2b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -570,7 +570,7 @@ module Nav = struct
   let restart _ = on_current_term restart
   let interrupt sn =
     Minilib.log "User break received";
-    Coq.break_coqtop sn.coqtop
+    Coq.break_coqtop sn.coqtop CString.(Set.elements (Map.domain sn.jobpage#data))
   let interrupt = cb_on_current_term interrupt
   let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document)
 end
diff --git a/ide/document.ml b/ide/document.ml
index bb431e791..62457fe56 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -16,8 +16,8 @@ type id = Stateid.t
 
 class type ['a] signals =
   object
-    method popped : callback:('a -> unit) -> unit
-    method pushed : callback:('a -> unit) -> unit
+    method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
+    method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
   end
 
 class ['a] signal () =
@@ -32,14 +32,14 @@ end
 type 'a document = {
   mutable stack : 'a sentence list;
   mutable context : ('a sentence list * 'a sentence list) option;
-  pushed_sig : 'a signal;
-  popped_sig : 'a signal;
+  pushed_sig : ('a * ('a list * 'a list) option) signal;
+  popped_sig : ('a * ('a list * 'a list) option) signal;
 }
 
-let connect d =
+let connect d : 'a signals =
   object
-    method pushed ~callback = d.pushed_sig#connect callback
-    method popped ~callback = d.popped_sig#connect callback
+    method pushed ~callback = d.pushed_sig#connect (fun (x, ctx) -> callback x ctx)
+    method popped ~callback = d.popped_sig#connect (fun (x, ctx) -> callback x ctx)
   end
 
 let create () = {
@@ -49,6 +49,12 @@ let create () = {
   popped_sig = new signal ();
 }
 
+let repr_context s = match s.context with
+| None -> None
+| Some (cl, cr) ->
+  let map s = s.data in
+  Some (List.map map cl, List.map map cr)
+
 (* Invariant, only the tip is a allowed to have state_id = None *)
 let invariant l = l = [] || (List.hd l).state_id <> None
 
@@ -64,12 +70,13 @@ let tip_data = function
 let push d x =
   assert(invariant d.stack);
   d.stack <- { data = x; state_id = None } :: d.stack;
-  d.pushed_sig#call x
+  d.pushed_sig#call (x, repr_context d)
 
 let pop = function
   | { stack = [] } -> raise Empty
-  | { stack = { data }::xs } as s -> s.stack <- xs; s.popped_sig#call data; data
-  
+  | { stack = { data }::xs } as s ->
+    s.stack <- xs; s.popped_sig#call (data, repr_context s); data
+
 let focus d ~cond_top:c_start ~cond_bot:c_stop =
   assert(invariant d.stack);
   if d.context <> None then invalid_arg "focus";
diff --git a/ide/document.mli b/ide/document.mli
index 0d803ff00..fb96cb6d7 100644
--- a/ide/document.mli
+++ b/ide/document.mli
@@ -108,8 +108,8 @@ val print :
 
 class type ['a] signals =
   object
-    method popped : callback:('a -> unit) -> unit
-    method pushed : callback:('a -> unit) -> unit
+    method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit
+    method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit
   end
 
 val connect : 'a document -> 'a signals
diff --git a/ide/session.ml b/ide/session.ml
index 058a422b9..cdec392ec 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -16,6 +16,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method data : 'a
   end
 
 class type control =
@@ -316,6 +317,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
           errs
       end
     method on_update ~callback:cb = callback := cb
+    method data = !last_update
   end
 
 let create_jobpage coqtop coqops : jobpage =
@@ -355,6 +357,7 @@ let create_jobpage coqtop coqops : jobpage =
           jobs
       end
     method on_update ~callback:cb = callback := cb
+    method data = !last_update
   end
 
 let create_proof () =
diff --git a/ide/session.mli b/ide/session.mli
index 8f7c79bec..028a1f9de 100644
--- a/ide/session.mli
+++ b/ide/session.mli
@@ -14,6 +14,7 @@ class type ['a] page =
     inherit GObj.widget
     method update : 'a -> unit
     method on_update : callback:('a -> unit) -> unit
+    method data : 'a
   end
 
 class type control =
diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml
index 71825d81e..c2799e40b 100644
--- a/ide/wg_Segment.ml
+++ b/ide/wg_Segment.ml
@@ -11,53 +11,13 @@ open Preferences
 
 type color = GDraw.color
 
-module Segment :
-sig
-  type +'a t
-  val length : 'a t -> int
-  val resize : 'a t -> int -> 'a t
-  val empty : 'a t
-  val add : int -> 'a -> 'a t -> 'a t
-  val remove : int -> 'a t -> 'a t
-  val fold : ('a -> 'a -> bool) -> (int -> int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-end =
-struct
-  type 'a t = {
-    length : int;
-    content : 'a Int.Map.t;
-  }
-
-  let empty = { length = 0; content = Int.Map.empty }
-
-  let length s = s.length
-
-  let resize s len =
-    if s.length <= len then { s with length = len }
-    else
-      let filter i v = i < len in
-      { length = len; content = Int.Map.filter filter s.content }
-
-  let add i v s =
-    if i < s.length then
-      { s with content = Int.Map.add i v s.content }
-    else s
-
-  let remove i s = { s with content = Int.Map.remove i s.content }
-
-  let fold eq f s accu =
-    let make k v (cur, accu) = match cur with
-    | None -> Some (k, k, v), accu
-    | Some (i, j, w) ->
-      if k = j + 1 && eq v w then Some (i, k, w), accu
-      else Some (k, k, v), (i, j, w) :: accu
-    in
-    let p, segments = Int.Map.fold make s.content (None, []) in
-    let segments = match p with
-    | None -> segments
-    | Some p -> p :: segments
-    in
-    List.fold_left (fun accu (i, j, v) -> f i j v accu) accu segments
+type model_event = [ `INSERT | `REMOVE | `SET of int * color ]
 
+class type model =
+object
+  method changed : callback:(model_event -> unit) -> unit
+  method length : int
+  method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
 end
 
 let i2f = float_of_int
@@ -96,7 +56,7 @@ object (self)
 
   val mutable width = 1
   val mutable height = 20
-  val mutable data = Segment.empty
+  val mutable model : model option = None
   val mutable default : color = `WHITE
   val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 ()
   val clicked = new GUtil.signal ()
@@ -114,10 +74,12 @@ object (self)
       end
     in
     let _ = box#misc#connect#size_allocate cb in
-    let clicked_cb ev =
+    let clicked_cb ev = match model with
+    | None -> true
+    | Some md ->
       let x = GdkEvent.Button.x ev in
       let (width, _) = pixmap#size in
-      let len = Segment.length data in
+      let len = md#length in
       let idx = f2i ((x *. i2f len) /. i2f width) in
       let () = clicked#call idx in
       true
@@ -128,17 +90,23 @@ object (self)
     (** Initial pixmap *)
     draw#set_pixmap pixmap
 
-  method length = Segment.length data
-
-  method set_length len =
-    data <- Segment.resize data len;
-    if self#misc#visible then self#refresh ()
+  method set_model md =
+    model <- Some md;
+    let changed_cb = function
+    | `INSERT | `REMOVE ->
+      if self#misc#visible then self#refresh ()
+    | `SET (i, color) ->
+      if self#misc#visible then self#fill_range color i (i + 1)
+    in
+    md#changed changed_cb
 
-  method private fill_range color i j =
+  method private fill_range color i j = match model with
+  | None -> ()
+  | Some md ->
     let i = i2f i in
     let j = i2f j in
     let width = i2f width in
-    let len = i2f (Segment.length data) in
+    let len = i2f md#length in
     let x = f2i ((i *. width) /. len) in
     let x' = f2i ((j *. width) /. len) in
     let w = x' - x in
@@ -146,14 +114,6 @@ object (self)
     pixmap#rectangle ~x ~y:0 ~width:w ~height ~filled:true ();
     draw#set_mask None;
 
-  method add i color =
-    data <- Segment.add i color data;
-    if self#misc#visible then self#fill_range color i (i + 1)
-
-  method remove i =
-    data <- Segment.remove i data;
-    if self#misc#visible then self#fill_range default i (i + 1)
-
   method set_default_color color = default <- color
   method default_color = default
 
@@ -162,11 +122,23 @@ object (self)
     draw#set_pixmap pixmap;
     self#refresh ();
 
-  method private refresh () =
+  method private refresh () = match model with
+  | None -> ()
+  | Some md ->
     pixmap#set_foreground default;
     pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true ();
-    let fold i j v () = self#fill_range v i (j + 1) in
-    Segment.fold color_eq fold data ();
+    let make (k, cur, accu) v = match cur with
+    | None -> pred k, Some (k, k, v), accu
+    | Some (i, j, w) ->
+      if k = j - 1 && color_eq v w then pred k, Some (k, i, w), accu
+      else pred k, Some (k, k, v), (i, j, w) :: accu
+    in
+    let _, p, segments = md#fold make (md#length - 1, None, []) in
+    let segments = match p with
+    | None -> segments
+    | Some p -> p :: segments
+    in
+    List.iter (fun (i, j, v) -> self#fill_range v i (j + 1)) segments;
     draw#set_mask None;
 
   method connect =
diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli
index 0fc8ebd75..29cbbedac 100644
--- a/ide/wg_Segment.mli
+++ b/ide/wg_Segment.mli
@@ -8,6 +8,8 @@
 
 type color = GDraw.color
 
+type model_event = [ `INSERT | `REMOVE | `SET of int * color ]
+
 class type segment_signals =
 object
   inherit GObj.misc_signals
@@ -15,15 +17,19 @@ object
   method clicked : callback:(int -> unit) -> GtkSignal.id
 end
 
+class type model =
+object
+  method changed : callback:(model_event -> unit) -> unit
+  method length : int
+  method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a
+end
+
 class segment : unit ->
   object
     inherit GObj.widget
     val obj : Gtk.widget Gtk.obj
+    method set_model : model -> unit
     method connect : segment_signals
-    method length : int
-    method set_length : int -> unit
     method default_color : color
     method set_default_color : color -> unit
-    method add : int -> color -> unit
-    method remove : int -> unit
   end
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 5f4f414a4..a382e9873 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1039,7 +1039,6 @@ module Goal = struct
     end
 
   let goals =
-    Env.get >>= fun env ->
     Pv.get >>= fun step ->
     let sigma = step.solution in
     let map goal =
@@ -1047,6 +1046,7 @@ module Goal = struct
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
         let gl =
+          Env.get >>= fun env ->
           tclEVARMAP >>= fun sigma ->
           tclUNIT (gmake env sigma goal)
         in
diff --git a/stm/stm.ml b/stm/stm.ml
index c4beb60e8..07262ef68 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -83,6 +83,18 @@ let async_proofs_workers_extra_env = ref [||]
 type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr }
 let pr_ast { expr } = pr_vernac expr
 
+(* Commands piercing opaque *)
+let may_pierce_opaque = function
+  | { expr = VernacPrint (PrintName _) } -> true
+  | { expr = VernacExtend (("Extraction",_), _) } -> true
+  | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true
+  | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true
+  | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true
+  | _ -> false
+
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 let vernac_interp ?proof id ?route { verbose; loc; expr } =
   let rec internal_command = function
@@ -145,7 +157,7 @@ type cmd_t = {
   ceff : bool; (* is a side-effecting command *)
   cast : ast;
   cids : Id.t list;
-  cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] }
+  cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] }
 type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list
 type qed_t = {
   qast : ast;
@@ -1662,7 +1674,7 @@ let delegate name =
   let time = get_hint_bp_time name in
   time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
               || !Flags.async_proofs_full
-
+ 
 let collect_proof keep cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
@@ -1684,23 +1696,20 @@ let collect_proof keep cur hd brkind id =
  let has_proof_no_using = function
    | Some (_, { expr = VernacProof(_,None) }) -> true
    | _ -> false in
- let may_pierce_opaque = function
-   | { expr = VernacPrint (PrintName _) } -> true
-   (* These do not exactly pierce opaque, but are anyway impossible to properly
-    * delegate *)
+ let too_complex_to_delegate = function
    | { expr = (VernacDeclareModule _
               | VernacDefineModule _
               | VernacDeclareModuleType _
               | VernacInclude _) } -> true
    | { expr =  (VernacRequire _ | VernacImport _) } -> true
-   | _ -> false in
+   | ast -> may_pierce_opaque ast in
  let parent = function Some (p, _) -> p | None -> assert false in
  let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
  let rec collect last accn id =
     let view = VCS.visit id in
     match view.step with
     | (`Sideff (`Ast(x,_)) | `Cmd { cast = x })
-      when may_pierce_opaque x -> `Sync(no_name,None,`Print)
+      when too_complex_to_delegate x -> `Sync(no_name,None,`Print)
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
     | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
@@ -1808,6 +1817,8 @@ let known_state ?(redefine_qed=false) ~cache id =
       | `Alias (id,_) -> (fun () ->
             reach view.next; reach id
           ), cache, true
+      | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () ->
+            reach view.next), cache, true
       | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () ->
             reach ~cache:`Shallow view.next;
             Hooks.(call tactic_being_run true); 
@@ -2173,6 +2184,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
           let id = VCS.new_node ~id:newtip () in
           let queue =
             if !Flags.async_proofs_full then `QueryQueue (ref false)
+            else if Flags.(!compilation_mode = BuildVio) &&
+                    VCS.((get_branch head).kind = `Master) &&
+                    may_pierce_opaque x
+                 then `SkipQueue 
             else `MainQueue in
           VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue });
           Backtrack.record (); if w == VtNow then finish (); `Ok
@@ -2251,7 +2266,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
                Proof_global.there_are_pending_proofs ()
             then begin
               let bname = VCS.mk_branch_name x in
-              VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[]));
+              let opacity_of_produced_term =
+                match x.expr with
+                | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
+                | _ -> Doesn'tGuaranteeOpacity in
+              VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
               VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode "Classic";
             end else begin
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 6e8e1a6d7..8123bd755 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -45,6 +45,10 @@ open Context.Named.Declaration
 let classes_dirpath =
   Names.DirPath.make (List.map Id.of_string ["Classes";"Coq"])
 
+let init_relation_classes () =
+  if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
+  else Coqlib.check_required_library ["Coq";"Classes";"RelationClasses"]
+
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
   else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"]
@@ -462,6 +466,8 @@ type hypinfo = {
 let get_symmetric_proof b = 
   if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
 
+let error_no_relation () = error "Cannot find a relation to rewrite."
+
 let rec decompose_app_rel env evd t = 
   (** Head normalize for compatibility with the old meta mechanism *)
   let t = Reductionops.whd_betaiota evd t in
@@ -477,8 +483,11 @@ let rec decompose_app_rel env evd t =
   | App (f, args) ->
     let len = Array.length args in
     let fargs = Array.sub args 0 (Array.length args - 2) in
-    mkApp (f, fargs), args.(len - 2), args.(len - 1)
-  | _ -> error "Cannot find a relation to rewrite."
+    let rel = mkApp (f, fargs) in
+    let ty = Retyping.get_type_of env evd rel in
+    let () = if not (Reduction.is_arity env ty) then error_no_relation () in
+    rel, args.(len - 2), args.(len - 1)
+  | _ -> error_no_relation ()
 
 let decompose_applied_relation env sigma (c,l) =
   let open Context.Rel.Declaration in
@@ -2059,8 +2068,9 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
 let not_declared env ty rel =
-  Tacticals.New.tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++
-		str ty ++ str" relation. Maybe you need to require the Setoid library")
+  Tacticals.New.tclFAIL 0
+    (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++
+     str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library")
 
 let setoid_proof ty fn fallback =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
@@ -2071,9 +2081,9 @@ let setoid_proof ty fn fallback =
       begin
         try
           let rel, _, _ = decompose_app_rel env sigma concl in
-          let evm = sigma in
           let open Context.Rel.Declaration in
-          let car = get_type (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in
+          let (sigma, t) = Typing.type_of env sigma rel in
+          let car = get_type (List.hd (fst (Reduction.dest_prod env t))) in
 	    (try init_setoid () with _ -> raise Not_found);
             fn env sigma car rel
         with e -> Proofview.tclZERO e
diff --git a/test-suite/bugs/closed/4574.v b/test-suite/bugs/closed/4574.v
new file mode 100644
index 000000000..39ba19036
--- /dev/null
+++ b/test-suite/bugs/closed/4574.v
@@ -0,0 +1,8 @@
+Require Import Setoid.
+
+Definition block A (a : A) := a.
+
+Goal forall A (a : A), block Type nat.
+Proof.
+Fail reflexivity.
+
diff --git a/test-suite/bugs/closed/4580.v b/test-suite/bugs/closed/4580.v
new file mode 100644
index 000000000..4ffd5f0f4
--- /dev/null
+++ b/test-suite/bugs/closed/4580.v
@@ -0,0 +1,6 @@
+Require Import Program.
+
+Class Foo (A : Type) := foo : A.
+
+Unset Refine Instance Mode.
+Program Instance f1 : Foo nat := S _.
diff --git a/test-suite/bugs/closed/4582.v b/test-suite/bugs/closed/4582.v
new file mode 100644
index 000000000..0842fb8fa
--- /dev/null
+++ b/test-suite/bugs/closed/4582.v
@@ -0,0 +1,10 @@
+Require List.
+Import List.ListNotations.
+
+Variable Foo : nat -> nat.
+
+Delimit Scope Foo_scope with F.
+
+Notation " [ x ] " := (Foo x) : Foo_scope.
+
+Check ([1] : nat)%F.
diff --git a/test-suite/vio/print.v b/test-suite/vio/print.v
new file mode 100644
index 000000000..9c36a463c
--- /dev/null
+++ b/test-suite/vio/print.v
@@ -0,0 +1,10 @@
+Lemma a : True.
+Proof.
+idtac.
+exact I.
+Qed.
+
+Print a.
+
+Lemma b : False.
+Admitted.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 62b01eb7d..b66699220 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -26,7 +26,7 @@ In a special module to avoid conflicts. *)
 Module ListNotations.
 Notation " [ ] " := nil (format "[ ]") : list_scope.
 Notation " [ x ] " := (cons x nil) : list_scope.
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
+Notation " [ x ; y ; .. ; z ] " :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
 End ListNotations.
 
 Import ListNotations.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2089bc944..898ef0d9e 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
 	  declare_instance_constant k pri global imps ?hook id pl
             poly evm (Option.get term) termtype
-	else if !refine_instance || Option.is_empty term then begin
+	else if Flags.is_program_mode () || !refine_instance || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	    if Flags.is_program_mode () then
 	      let hook vis gr _ =