Merge branch 'v8.5'

38 files changed, 191 insertions, 153 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 8495156ca..b03aa6409 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -755,19 +755,19 @@ the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}).
  E.g. in this case (this occurs only in the {\tt Set}-impredicative
  variant of \Coq):
 
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
 \begin{coq_example*}
 Inductive I : Type :=
   intro : forall k:Set, k -> I.
-Lemma eq_jdef : 
+Lemma eq_jdef :
    forall x y:nat, intro _ x = intro _ y -> x = y.
 Proof.
    intros x y H; injection H.
 \end{coq_example*}
 
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
  Injectivity of constructors is restricted to predicative types. If
 injectivity on large inductive types were not restricted, we would be
 allowed to derive an inconsistency (e.g. following the lines of
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 67e4bdb0c..5892fb3d9 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -311,7 +311,7 @@ let read_buffer = Buffer.create maxread
     I/O Exceptions are propagated. *)
 
 let read_file name buf =
-  let ic = open_in name in
+  let ic = Util.open_utf8_file_in name in
   let len = ref 0 in
   try
     while len := input ic read_string 0 maxread; !len > 0 do
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 982d9bfe3..8c56d0ccf 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1120,7 +1120,7 @@ let drop_notations_pattern looked_for =
 	      let (argscs,_) = find_remaining_scopes pats [] g in
 	      Some (g, List.map2 (in_pat_sc env) argscs pats, [])
 	| NApp (NRef g,args) ->
-	      ensure_kind top loc g;
+	      test_kind top g;
 	      let nvars = List.length vars in
 	      if List.length pats < nvars then error_not_enough_arguments loc;
 	      let pats1,pats2 = List.chop nvars pats in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index e304725d4..87f7a6d6e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -245,21 +245,21 @@ let combine_params_freevar =
 
 let destClassApp cl =
   match cl with
-    | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l
-    | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l
-    | CRef (ref,_) -> loc_of_reference ref, ref, []
+    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, List.map fst l, inst
+    | CAppExpl (loc, (None, ref, inst), l) -> loc, ref, l, inst
+    | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
 let destClassAppExpl cl =
   match cl with
-    | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l
-    | CRef (ref,_) -> loc_of_reference ref, ref, []
+    | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, l, inst
+    | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
     | _ -> raise Not_found
 
 let implicit_application env ?(allow_partial=true) f ty =
   let is_class =
     try
-      let (loc, r, _ as clapp) = destClassAppExpl ty in
+      let (_, r, _, _ as clapp) = destClassAppExpl ty in
       let (loc, qid) = qualid_of_reference r in
       let gr = Nametab.locate qid in
 	if Typeclasses.is_class gr then Some (clapp, gr) else None
@@ -267,7 +267,7 @@ let implicit_application env ?(allow_partial=true) f ty =
   in
     match is_class with
     | None -> ty, env
-    | Some ((loc, id, par), gr) ->
+    | Some ((loc, id, par, inst), gr) ->
 	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
 	  let c = class_info gr in
@@ -285,7 +285,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	    end;
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
-	    CAppExpl (loc, (None, id, None), args), avoid
+	    CAppExpl (loc, (None, id, inst), args), avoid
 	in c, avoid
 
 let implicits_of_glob_constr ?(with_products=true) l =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 818f7e9a8..a3721af66 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -16,8 +16,8 @@ open Globnames
 val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> Loc.t * reference * constr_expr list
-val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list
+val destClassApp : constr_expr -> Loc.t * reference * constr_expr list * instance_expr option
+val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list * instance_expr option
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d5435f0c3..3462694d6 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -524,14 +524,14 @@ let rec compile_fv reloc l sz cont =
 
 (* Compiling constants *)
 
-let rec get_allias env (kn,u as p) =
+let rec get_alias env (kn,u as p) =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
     match tps with
     | None -> p
     | Some tps ->
        (match Cemitcodes.force tps with
-	| BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
+	| BCalias (kn',u') -> get_alias env (kn', Univ.subst_instance_instance u u')
 	| _ -> p)
 
 (* Compiling expressions *)
@@ -756,10 +756,10 @@ and compile_const =
                   (mkConstU (kn,u)) reloc args sz cont
   with Not_found ->
     if Int.equal nargs 0 then
-      Kgetglobal (get_allias !global_env (kn, u)) :: cont
+      Kgetglobal (get_alias !global_env (kn, u)) :: cont
     else
       comp_app (fun _ _ _ cont ->
-                   Kgetglobal (get_allias !global_env (kn,u)) :: cont)
+                   Kgetglobal (get_alias !global_env (kn,u)) :: cont)
         compile_constr reloc () args sz cont
 
 let compile fail_on_error env c =
@@ -797,14 +797,14 @@ let compile_constant_body fail_on_error env = function
 	| Const (kn',u) ->
 	    (* we use the canonical name of the constant*)
 	    let con= constant_of_kn (canonical_con kn') in
-	      Some (BCallias (get_allias env (con,u)))
+	      Some (BCalias (get_alias env (con,u)))
 	| _ ->
 	    let res = compile fail_on_error env body in
 	      Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
 
-let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
+let compile_alias (kn,u) = BCalias (constant_of_kn (canonical_con kn), u)
 
 (* spiwack: additional function which allow different part of compilation of the
       31-bit integers *)
@@ -867,7 +867,7 @@ let op2_compilation op =
          Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
-          (*Kgetglobal (get_allias !global_env kn):: *)
+          (*Kgetglobal (get_alias !global_env kn):: *)
           normal::
           Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
      in
@@ -886,7 +886,7 @@ let op2_compilation op =
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = 2 and non-tailcall cont*)
-           (*Kgetglobal (get_allias !global_env kn):: *)
+           (*Kgetglobal (get_alias !global_env kn):: *)
            normal::
            Kapply 2::labeled_cont)))
   else if nargs=0 then
@@ -900,7 +900,7 @@ let op2_compilation op =
   1/ checks if all the arguments are constants (i.e. non-block values)
   2/ if they are, uses the "op" instruction to execute
   3/ if at least one is not, branches to the normal behavior:
-      Kgetglobal (get_allias !global_env kn) *)
+      Kgetglobal (get_alias !global_env kn) *)
 let op_compilation n op =
   let code_construct kn cont =
      let f_cont =
@@ -908,7 +908,7 @@ let op_compilation n op =
          Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
-          Kgetglobal (get_allias !global_env kn)::
+          Kgetglobal (get_alias !global_env kn)::
           Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
      in
      let lbl = Label.create () in
@@ -926,7 +926,7 @@ let op_compilation n op =
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = n and non-tailcall cont*)
-           Kgetglobal (get_allias !global_env kn)::
+           Kgetglobal (get_alias !global_env kn)::
            Kapply n::labeled_cont)))
   else if Int.equal nargs 0 then
     code_construct kn cont
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 6dbfbe9cc..9b275cb6c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -328,36 +328,36 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of pconstant
+  | BCalias of pconstant
   | BCconstant
 
 type to_patch_substituted =
 | PBCdefined of to_patch substituted
-| PBCallias of pconstant substituted
+| PBCalias of pconstant substituted
 | PBCconstant
 
 let from_val = function
 | BCdefined tp -> PBCdefined (from_val tp)
-| BCallias cu -> PBCallias (from_val cu)
+| BCalias cu -> PBCalias (from_val cu)
 | BCconstant -> PBCconstant
 
 let force = function
 | PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_pconstant cu)
 | PBCconstant -> BCconstant
 
 let subst_to_patch_subst s = function
 | PBCdefined tp -> PBCdefined (subst_substituted s tp)
-| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCalias cu -> PBCalias (subst_substituted s cu)
 | PBCconstant -> PBCconstant
 
 let repr_body_code = function
 | PBCdefined tp ->
   let (s, tp) = repr_substituted tp in
   (s, BCdefined tp)
-| PBCallias cu ->
+| PBCalias cu ->
   let (s, cu) = repr_substituted cu in
-  (s, BCallias cu)
+  (s, BCalias cu)
 | PBCconstant -> (None, BCconstant)
 
 let to_memory (init_code, fun_code, fv) =
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index cec901306..54b92b912 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of constant Univ.puniverses
+  | BCalias of constant Univ.puniverses
   | BCconstant
 
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8fd90ec36..b3f0ba5b5 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -163,7 +163,7 @@ let rec slot_for_getglobal env (kn,u) =
 	    let v = eval_to_patch env (code,pl,fv) in
 	      set_global v
 	    else set_global (val_of_constant (kn,u))
-	 | BCallias kn' -> slot_for_getglobal env kn'
+	 | BCalias kn' -> slot_for_getglobal env kn'
 	 | BCconstant -> set_global (val_of_constant (kn,u)) in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (Ephemeron.create pos);
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 90c437bbf..687b740f6 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2012,7 +2012,7 @@ let rec compile_deps env sigma prefix ~interactive init t =
   match kind_of_term t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
-      let c,u = get_allias env c in
+      let c,u = get_alias env c in
       let cb,(nameref,_) = lookup_constant_key c env in
       let (_, (_, const_updates)) = init in
       if is_code_loaded ~interactive nameref
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 383f81029..cb08b5058 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -373,13 +373,13 @@ let makeblock env cn u tag args =
 
 (* Translation of constants *)
 
-let rec get_allias env (kn, u as p) =
+let rec get_alias env (kn, u as p) =
   let tps = (lookup_constant kn env).const_body_code in
     match tps with
     | None -> p
     | Some tps ->
        match Cemitcodes.force tps with
-       | Cemitcodes.BCallias kn' -> get_allias env kn'
+       | Cemitcodes.BCalias kn' -> get_alias env kn'
        | _ -> p
 
 (*i Global environment *)
@@ -651,7 +651,7 @@ let rec lambda_of_constr env sigma c =
 and lambda_of_app env sigma f args =
   match kind_of_term f with
   | Const (kn,u as c) ->
-      let kn,u = get_allias !global_env c in
+      let kn,u = get_alias !global_env c in
       let cb = lookup_constant kn !global_env in
       (try
           let prefix = get_const_prefix !global_env kn in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index ccf2888b5..3b6fafbbc 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -26,7 +26,7 @@ val mk_lazy : lambda -> lambda
 
 val get_mind_prefix : env -> mutual_inductive -> string
 
-val get_allias : env -> pconstant -> pconstant
+val get_alias : env -> pconstant -> pconstant
 
 val lambda_of_constr : env -> evars -> Constr.constr -> lambda
 
diff --git a/lib/util.ml b/lib/util.ml
index a8c25f745..a20dba0fc 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -132,3 +132,14 @@ let map_union f g = function
 type iexn = Exninfo.iexn
 
 let iraise = Exninfo.iraise
+
+let open_utf8_file_in fname =
+  let is_bom s =
+    Int.equal (Char.code s.[0]) 0xEF &&
+    Int.equal (Char.code s.[1]) 0xBB &&
+    Int.equal (Char.code s.[2]) 0xBF
+  in
+  let in_chan = open_in fname in
+  let s = "   " in
+  if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
+  in_chan
diff --git a/lib/util.mli b/lib/util.mli
index 4fce809c2..1dc405fcb 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -110,3 +110,6 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
 
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
+
+val open_utf8_file_in : string -> in_channel
+(** Open an utf-8 encoded file and skip the byte-order mark if any. *)
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
index a33be9da7..f6943dd13 100644
--- a/lib/xml_lexer.mll
+++ b/lib/xml_lexer.mll
@@ -281,6 +281,11 @@ and dq_string = parse
                         Buffer.add_char tmp (lexeme_char lexbuf 1);
                         dq_string lexbuf
                 }
+        | '&'
+                {
+                        Buffer.add_string tmp (entity lexbuf);
+                        dq_string lexbuf
+                }
         | eof
                 { raise (Error EUnterminatedString) }
         | _
@@ -297,6 +302,11 @@ and q_string = parse
                         Buffer.add_char tmp (lexeme_char lexbuf 1);
                         q_string lexbuf
                 }
+        | '&'
+                {
+                        Buffer.add_string tmp (entity lexbuf);
+                        q_string lexbuf
+                }
         | eof
                 { raise (Error EUnterminatedString) }
         | _
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
index eeddd53cb..bbb7b51ba 100644
--- a/lib/xml_printer.ml
+++ b/lib/xml_printer.ml
@@ -46,6 +46,8 @@ let buffer_attr tmp (n,v) =
     match v.[p] with
       | '\\' -> output "\\\\"
       | '"' -> output "\\\""
+      | '<' -> output "&lt;"
+      | '&' -> output "&amp;"
       | c -> output' c
   done;
   output' '"'
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9c041d72c..d024c01ba 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -42,7 +42,7 @@ let cook_this_proof p =
 
 let cook_proof () =
   cook_this_proof (fst
-    (Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)))
+    (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
 let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8677b854d..c02b90916 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -269,7 +269,7 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
+let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
@@ -290,7 +290,7 @@ let close_proof ~keep_body_ucst_sepatate ?feedback_id ~now fpl =
         let body = c and typ = nf t in
         let used_univs_body = Universes.universes_of_constr body in
         let used_univs_typ = Universes.universes_of_constr typ in
-        if keep_body_ucst_sepatate then
+        if keep_body_ucst_separate then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
           let ctx = Evd.evar_universe_context_set initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
@@ -379,9 +379,9 @@ let return_proof ?(allow_partial=false) () =
     proofs, Evd.evar_universe_context evd
 
 let close_future_proof ~feedback_id proof =
-  close_proof ~keep_body_ucst_sepatate:true ~feedback_id ~now:false proof
-let close_proof ~keep_body_ucst_sepatate fix_exn =
-  close_proof ~keep_body_ucst_sepatate ~now:true
+  close_proof ~keep_body_ucst_separate:true ~feedback_id ~now:false proof
+let close_proof ~keep_body_ucst_separate fix_exn =
+  close_proof ~keep_body_ucst_separate ~now:true
     (Future.from_val ~fix_exn (return_proof ()))
 
 (** Gets the current terminator without checking that the proof has
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 88e047782..b5dd5ef85 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -91,7 +91,7 @@ val start_dependent_proof :
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
-val close_proof : keep_body_ucst_sepatate:bool -> Future.fix_exn -> closed_proof
+val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof
 
 (* Intermediate step necessary to delegate the future.
  * Both access the current proof state. The formes is supposed to be
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 64ea5aea0..11b7d07d0 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -648,7 +648,7 @@ let goodmod p m =
 
 let cycle n =
   let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle"++spc()++int n))) >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle "++int n))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let n' = goodmod n l in
@@ -658,7 +658,7 @@ let cycle n =
 
 let swap i j =
   let open Proof in
-  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"swap"++spc()++int i++spc()++int j))) >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"swap"++spc()++int i++spc()++int j)))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
@@ -1057,7 +1057,7 @@ struct
     let comb = undefined sigma (CList.rev evs) in
     let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
-    InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >>
+    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
     Pv.set { solution = sigma; comb; }
   end
 
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index c766f3fab..6c8630404 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -503,7 +503,7 @@ let save_proof ?proof = function
       let (proof_obj,terminator) =
         match proof with
         | None ->
-            Proof_global.close_proof ~keep_body_ucst_sepatate:false (fun x -> x)
+            Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)
         | Some proof -> proof
       in
       (* if the proof is given explicitly, nothing has to be deleted *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 8af1aaafd..9e82dd156 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1220,7 +1220,7 @@ end = struct (* {{{ *)
         (Lemmas.standard_proof_terminator []
           (Lemmas.mk_hook (fun _ _ -> ())));
       let proof =
-        Proof_global.close_proof ~keep_body_ucst_sepatate:true (fun x -> x) in
+        Proof_global.close_proof ~keep_body_ucst_separate:true (fun x -> x) in
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
       Reach.known_state ~cache:`No start;
@@ -1854,7 +1854,7 @@ let known_state ?(redefine_qed=false) ~cache id =
                       qed.fproof <- Some (fp, ref false); None
                   | VtKeep ->
                       Some(Proof_global.close_proof
-                                ~keep_body_ucst_sepatate:false
+                                ~keep_body_ucst_separate:false
                                 (State.exn_on id ~valid:eop)) in
                 reach view.next;
                 if keep == VtKeepAsAxiom then
@@ -2451,7 +2451,7 @@ let get_script prf =
   let branch, test =
     match prf with
     | None -> VCS.Branch.master, fun _ -> true
-    | Some name -> VCS.current_branch (),  List.mem name in
+    | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in
   let rec find acc id =
     if Stateid.equal id Stateid.initial ||
        Stateid.equal id Stateid.dummy then acc else
@@ -2462,7 +2462,9 @@ let get_script prf =
     | `Sideff (`Ast (x,_)) ->
          find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
     | `Sideff (`Id id)  -> find acc id
-    | `Cmd {cast = x} -> find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
+    | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
+         find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
+    | `Cmd _ -> find acc view.next
     | `Alias (id,_) -> find acc id
     | `Fork _ -> find acc view.next
     in
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index a5d68e19b..4fb76bb82 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -104,22 +104,29 @@ let mkGenDecideEqGoal rectype g =
         (mkDecideEqGoal true (build_coq_sumbool ())
           rectype (mkVar xname) (mkVar yname))))
 
+let rec rewrite_and_clear hyps = match hyps with
+| [] -> Proofview.tclUNIT ()
+| id :: hyps ->
+  tclTHENLIST [
+    Equality.rewriteLR (mkVar id);
+    clear [id];
+    rewrite_and_clear hyps;
+  ]
+
 let eqCase tac =
-  (tclTHEN intro
-  (tclTHEN (onLastHyp Equality.rewriteLR)
-  (tclTHEN clear_last
-  tac)))
+  tclTHEN intro (onLastHypId tac)
 
-let diseqCase eqonleft =
+let diseqCase hyps eqonleft =
   let diseq  = Id.of_string "diseq" in
   let absurd = Id.of_string "absurd" in
   (tclTHEN (intro_using diseq)
   (tclTHEN (choose_noteq eqonleft)
+  (tclTHEN (rewrite_and_clear (List.rev hyps))
   (tclTHEN  (Proofview.V82.tactic red_in_concl)
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (Simple.apply (mkVar diseq))
   (tclTHEN  (Extratactics.injHyp absurd)
-            (full_trivial [])))))))
+            (full_trivial []))))))))
 
 open Proofview.Notations
 
@@ -131,15 +138,24 @@ let match_eqdec c =
 
 (* /spiwack *)
 
-let solveArg eqonleft op a1 a2 tac =
+let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
+| [], [] ->
+  tclTHENLIST [
+    choose_eq eqonleft;
+    rewrite_and_clear (List.rev hyps);
+    intros_reflexivity;
+  ]
+| a1 :: largs, a2 :: rargs ->
   Proofview.Goal.enter begin fun gl ->
   let rectype = pf_unsafe_type_of gl a1 in
   let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
+  let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
   let subtacs =
-    if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
-    else [diseqCase eqonleft;eqCase tac;default_auto] in
+    if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
+    else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
   (tclTHENS (elim_type decide) subtacs)
   end
+| _ -> invalid_arg "List.fold_right2"
 
 let solveEqBranch rectype =
   Proofview.tclORELSE
@@ -152,9 +168,7 @@ let solveEqBranch rectype =
           let getargs l = List.skipn nparams (snd (decompose_app l)) in
           let rargs   = getargs rhs
           and largs   = getargs lhs in
-          List.fold_right2
-            (solveArg eqonleft op) largs rargs
-            (tclTHEN (choose_eq eqonleft) intros_reflexivity)
+          solveArg [] eqonleft op largs rargs
       end
     end
     begin function (e, info) -> match e with
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e79fc6dc9..65239a5f7 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -98,8 +98,8 @@ struct
   | DSort, DSort -> 0
   | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
   | DCtx (tl1, tr1), DCtx (tl2, tr2)
-  | DLambda (tl1, tr1), DCtx (tl2, tr2)
-  | DApp (tl1, tr1), DCtx (tl2, tr2) ->
+  | DLambda (tl1, tr1), DLambda (tl2, tr2)
+  | DApp (tl1, tr1), DApp (tl2, tr2) ->
     let c = cmp tl1 tl2 in
     if c = 0 then cmp tr1 tr2 else c
 
diff --git a/test-suite/bugs/closed/2243.v b/test-suite/bugs/closed/2243.v
new file mode 100644
index 000000000..6d45c9a09
--- /dev/null
+++ b/test-suite/bugs/closed/2243.v
@@ -0,0 +1,9 @@
+Inductive is_nul: nat -> Prop := X: is_nul 0.
+Section O.
+Variable u: nat.
+Variable H: is_nul u.
+Goal True.
+Proof.
+destruct H.
+Undo.
+revert H; intro H; destruct H.
diff --git a/test-suite/bugs/closed/3509.v b/test-suite/bugs/closed/3509.v
new file mode 100644
index 000000000..822662267
--- /dev/null
+++ b/test-suite/bugs/closed/3509.v
@@ -0,0 +1,6 @@
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 : bar.
+Hint Rewrite a2 : bar.
diff --git a/test-suite/bugs/closed/3510.v b/test-suite/bugs/closed/3510.v
new file mode 100644
index 000000000..4cbae3359
--- /dev/null
+++ b/test-suite/bugs/closed/3510.v
@@ -0,0 +1,5 @@
+Inductive T := Foo : T.
+Axiom (b : T) (R : forall x : T, Prop) (f : forall x : T, R x).
+Axiom a1 : match b with Foo => f end = f.
+Axiom a2 : match b with Foo => f b end = f b.
+Hint Rewrite a1 a2 : bar.
diff --git a/test-suite/bugs/closed/3736.v b/test-suite/bugs/closed/3736.v
new file mode 100644
index 000000000..637b77cc5
--- /dev/null
+++ b/test-suite/bugs/closed/3736.v
@@ -0,0 +1,8 @@
+(* Check non-error failure in case of unsupported decidability scheme *)
+Local Set Decidable Equality Schemes.
+
+Inductive a := A with b := B.
+
+(* But fails with error if explicitly asked for the scheme *)
+
+Fail Scheme Equality for a.
diff --git a/test-suite/bugs/closed/4280.v b/test-suite/bugs/closed/4280.v
new file mode 100644
index 000000000..fd7897509
--- /dev/null
+++ b/test-suite/bugs/closed/4280.v
@@ -0,0 +1,24 @@
+Require Import ZArith.
+Require Import Eqdep_dec.
+Local Open Scope Z_scope.
+
+Definition t := { n: Z | n > 1 }.
+
+Program Definition two : t := 2.
+Next Obligation. omega. Qed.
+
+Program Definition t_eq (x y: t) : {x=y} + {x<>y} :=
+  if Z.eq_dec (proj1_sig x) (proj1_sig y) then left _ else right _.
+Next Obligation.
+  destruct x as [x Px], y as [y Py]. simpl in H; subst y.
+  f_equal. apply UIP_dec. decide equality.
+Qed.
+Next Obligation.
+  congruence.
+Qed.
+
+Definition t_list_eq: forall (x y: list t), {x=y} + {x<>y}.
+Proof. decide equality. apply t_eq. Defined.
+
+Goal match t_list_eq (two::nil) (two::nil) with left _ => True | right _ => False end.
+Proof. exact I. Qed.
diff --git a/test-suite/bugs/closed/4305.v b/test-suite/bugs/closed/4305.v
new file mode 100644
index 000000000..39fc02d22
--- /dev/null
+++ b/test-suite/bugs/closed/4305.v
@@ -0,0 +1,17 @@
+(* Check fallback when an abbreviation is not interpretable as a pattern *)
+
+Notation foo := Type.
+
+Definition t :=
+  match 0 with
+  | S foo => foo
+  | _ => 0
+  end.
+
+Notation bar := (option Type).
+
+Definition u :=
+  match 0 with
+  | S bar => bar
+  | _ => 0
+  end.
diff --git a/test-suite/bugs/opened/3509.v b/test-suite/bugs/opened/3509.v
deleted file mode 100644
index 3913bbb43..000000000
--- a/test-suite/bugs/opened/3509.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import TestSuite.admit.
-Lemma match_bool_fn b A B xT xF
-: match b as b return forall x : A, B b x with
-    | true => xT
-    | false => xF
-  end
-  = fun x : A => match b as b return B b x with
-                   | true => xT x
-                   | false => xF x
-                 end.
-admit.
-Defined.
-Lemma match_bool_comm_1 (b : bool) A B (F : forall x : A, B x) t f
-: (if b as b return B (if b then t else f) then F t else F f)
-  = F (if b then t else f).
-admit.
-Defined.
-Hint Rewrite match_bool_fn : matchdb.
-Fail Hint Rewrite match_bool_comm_1 : matchdb.
diff --git a/test-suite/bugs/opened/3510.v b/test-suite/bugs/opened/3510.v
deleted file mode 100644
index daf265071..000000000
--- a/test-suite/bugs/opened/3510.v
+++ /dev/null
@@ -1,35 +0,0 @@
-Require Import TestSuite.admit.
-Lemma match_option_fn T (b : option T) A B s n
-: match b as b return forall x : A, B b x with
-    | Some k => s k
-    | None => n
-  end
-  = fun x : A => match b as b return B b x with
-                   | Some k => s k x
-                   | None => n x
-                 end.
-admit.
-Defined.
-Lemma match_option_comm_2 T (p : option T) A B R (f : forall (x : A) (y : B x), R x y) (s1 : T -> A) (s2 : forall x : T, B (s1 x)) n1 n2
-: match p as p return R match p with
-                          | Some k => s1 k
-                          | None => n1
-                        end
-                        match p as p return B match p with Some k => s1 k | None => n1 end with
-                          | Some k => s2 k
-                          | None => n2
-                        end with
-    | Some k => f (s1 k) (s2 k)
-    | None => f n1 n2
-  end
-  = f match p return A with
-        | Some k => s1 k
-        | None => n1
-      end
-      match p as p return B match p with Some k => s1 k | None => n1 end with
-        | Some k => s2 k
-        | None => n2
-      end.
-admit.
-Defined.
-Fail Hint Rewrite match_option_fn match_option_comm_2 : matchdb.
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 7f2fe741e..fc652f584 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -68,7 +68,7 @@ let begin_coq_example =
 let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
 let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
 let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
-let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
+let dot_end_line = Str.regexp "\\(\\.\\|}\\)[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
 
 let has_match r s =
   try let _ = Str.search_forward r s 0 in true with Not_found -> false
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f90508090..d1452fca2 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -55,6 +55,7 @@ exception InductiveWithProduct
 exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
+exception DecidabilityMutualNotSupported
 
 let dl = Loc.ghost
 
@@ -921,7 +922,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 let make_eq_decidability mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
-    anomaly (Pp.str "Decidability lemma for mutual inductive types not supported");
+    raise DecidabilityMutualNotSupported;
   let ind = (mind,0) in
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 807872988..20a3d5d74 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -23,6 +23,7 @@ exception InductiveWithProduct
 exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
+exception DecidabilityMutualNotSupported
 
 val beq_scheme_kind : mutual scheme_kind
 val build_beq_scheme : mutual_scheme_object_function
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index fbc45b4ae..286d164c4 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -180,10 +180,12 @@ let try_declare_scheme what f internal names kn =
 	  (strbrk "Required constant " ++ str s ++ str " undefined.")
     | AlreadyDeclared msg ->
         alarm what internal (msg ++ str ".")
+    | DecidabilityMutualNotSupported ->
+        alarm what internal
+          (str "Decidability lemma for mutual inductive types not supported.")
     | e when Errors.noncritical e ->
-	alarm what internal
-	  (str "Unknown exception during scheme creation: "++
-           str (Printexc.to_string e))
+        alarm what internal
+	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
 
 let beq_scheme_msg mind =
   let mib = Global.lookup_mind mind in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 966b95201..266d8f9b4 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -92,19 +92,6 @@ let disable_drop = function
 
 let user_error loc s = Errors.user_err_loc (loc,"_",str s)
 
-(* Open an utf-8 encoded file and skip the byte-order mark if any *)
-
-let open_utf8_file_in fname =
-  let is_bom s =
-    Int.equal (Char.code s.[0]) 0xEF &&
-    Int.equal (Char.code s.[1]) 0xBB &&
-    Int.equal (Char.code s.[2]) 0xBF
-  in
-  let in_chan = open_in fname in
-  let s = "   " in
-  if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
-  in_chan
-
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
    Note: we could use only one thanks to seek_in, but seeking on and on in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6c5f10c20..cfbdaccec 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1841,16 +1841,6 @@ let vernac_load interp fname =
     match Pcoq.Gram.entry_parse Pcoq.main_entry po with
       | Some x -> x
       | None -> raise End_of_input) in
-  let open_utf8_file_in fname =
-    let is_bom s =
-      Int.equal (Char.code s.[0]) 0xEF &&
-      Int.equal (Char.code s.[1]) 0xBB &&
-      Int.equal (Char.code s.[2]) 0xBF
-    in
-    let in_chan = open_in fname in
-    let s = "   " in
-    if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0;
-    in_chan in
   let fname =
     Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
   let fname = CUnix.make_suffix fname ".v" in