Merge branch 'v8.6'

24 files changed, 482 insertions, 139 deletions

diff --git a/library/loadpath.ml b/library/loadpath.ml
index e6f6716c3..d03c6c555 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -72,9 +72,6 @@ let add_load_path phys_path coq_path ~implicit =
     let replace =
       if DirPath.equal coq_path old_path then
         implicit <> old_implicit
-      else if DirPath.equal coq_path (Nameops.default_root_prefix)
-              && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then
-        false (* This is the default "-I ." path, don't override the old path *)
       else
         let () =
           (* Do not warn when overriding the default "-I ." path *)
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index d551b7315..f8654d390 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -44,18 +44,10 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug
 | [ ] -> [ false ]
 END
 
-let pr_depth _prc _prlc _prt = function
-    Some i -> Pp.int i
-  | None -> Pp.mt()
-
-ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth
-  | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ]
-END
-
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [
+ | [ "Typeclasses" "eauto" ":=" debug(d) int_opt(depth) ] -> [
      set_typeclasses_debug d;
      set_typeclasses_depth depth
    ]
@@ -63,9 +55,9 @@ END
 
 (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *)
 TACTIC EXTEND typeclasses_eauto
- | [ "typeclasses" "eauto" depth(d) "with" ne_preident_list(l) ] ->
+ | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] ->
     [ typeclasses_eauto d l ]
- | [ "typeclasses" "eauto" depth(d) ] -> [
+ | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [
      typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ]
 END
 
diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml
index fe591c775..102918e5e 100644
--- a/ltac/profile_ltac.ml
+++ b/ltac/profile_ltac.ml
@@ -166,7 +166,7 @@ let rec print_node ~filter all_total indent prefix (s, e) =
 and print_table ~filter all_total indent first_level table =
   let fold _ n l =
     let s, total = n.name, n.total in
-    if filter s then (s, n) :: l else l in
+    if filter s total then (s, n) :: l else l in
   let ls = M.fold fold table [] in
   match ls with
   | [s, n] when not first_level ->
@@ -182,7 +182,7 @@ and print_table ~filter all_total indent first_level table =
     in
     prlist (fun pr -> pr) (list_iter_is_last iter ls)
 
-let to_string ~filter node =
+let to_string ~filter ?(cutoff=0.0) node =
   let tree = node.children in
   let all_total = M.fold (fun _ { total } a -> total +. a) node.children 0.0 in
   let flat_tree =
@@ -218,6 +218,7 @@ let to_string ~filter node =
     !global
   in
   warn_encountered_multi_success_backtracking ();
+  let filter s n = filter s && n >= cutoff in
   let msg =
     h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
     fnl () ++
@@ -387,22 +388,24 @@ let reset_profile () =
 
 (* ******************** *)
 
-let print_results_filter ~filter =
+let print_results_filter ~cutoff ~filter =
   let valid id _ = Stm.state_of_id id <> `Expired in
   data := SM.filter valid !data;
   let results =
     SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in
   let results = merge_roots results Local.(CList.last !stack) in
-  Feedback.msg_notice (to_string ~filter results)
+  Feedback.msg_notice (to_string ~cutoff ~filter results)
 ;;
 
-let print_results () = print_results_filter ~filter:(fun _ -> true)
+let print_results ~cutoff =
+  print_results_filter ~cutoff ~filter:(fun _ -> true)
 
 let print_results_tactic tactic =
-  print_results_filter ~filter:(fun s ->
+  print_results_filter ~cutoff:0.0 ~filter:(fun s ->
     String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic)))))
 
-let do_print_results_at_close () = if get_profiling () then print_results ()
+let do_print_results_at_close () =
+  if get_profiling () then print_results ~cutoff:0.0
 
 let _ = Declaremods.append_end_library_hook do_print_results_at_close
 
diff --git a/ltac/profile_ltac.mli b/ltac/profile_ltac.mli
index 8c4b47b8e..e5e2e4197 100644
--- a/ltac/profile_ltac.mli
+++ b/ltac/profile_ltac.mli
@@ -14,7 +14,8 @@ val do_profile :
 
 val set_profiling : bool -> unit
 
-val print_results : unit -> unit
+(* Cut off results < than specified cutoff *)
+val print_results : cutoff:float -> unit
 
 val print_results_tactic : string -> unit
 
diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4
index c092a0cb6..9083bda60 100644
--- a/ltac/profile_ltac_tactics.ml4
+++ b/ltac/profile_ltac_tactics.ml4
@@ -31,7 +31,8 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
-  [ "Show" "Ltac" "Profile" ] -> [ print_results() ]
+| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ]
+| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ]
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 482ce5053..7c2178222 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -127,11 +127,11 @@ type polynom =
     num : int;
     sugar : int}
 
-let nvar m =  Array.length m - 1
+let nvar (m : mon) =  Array.length m - 1
 
-let deg m = m.(0)
+let deg (m : mon) = m.(0)
 
-let mult_mon m m' =
+let mult_mon (m : mon) (m' : mon) =
   let d = nvar m in
   let m'' = Array.make (d+1) 0 in
   for i=0 to d do
@@ -140,7 +140,7 @@ let mult_mon m m' =
   m''
 
 
-let compare_mon m m' =
+let compare_mon (m : mon) (m' : mon) =
   let d = nvar m in
   if !lexico
   then (
@@ -148,18 +148,18 @@ let compare_mon m m' =
     let res=ref 0 in
     let i=ref 1 in (* 1 si lexico pur 0 si degre*)
     while (!res=0) && (!i<=d) do
-      res:= (compare m.(!i) m'.(!i));
+      res:= (Int.compare m.(!i) m'.(!i));
       i:=!i+1;
     done;
     !res)
   else (
      (* degre lexicographique inverse *)
-    match compare m.(0) m'.(0) with
+    match Int.compare m.(0) m'.(0) with
     | 0 -> (* meme degre total *)
 	let res=ref 0 in
 	let i=ref d in
 	while (!res=0) && (!i>=1) do
-	  res:= - (compare m.(!i) m'.(!i));
+	  res:= - (Int.compare m.(!i) m'.(!i));
 	  i:=!i-1;
 	done;
 	!res
@@ -402,29 +402,25 @@ let polconst d c =
   [(c,m)]
 
 let plusP p q =
-  let rec plusP p q =
-    match p with
-      [] -> q
-    |t::p' -> 
-	match q with
-	  [] -> p
-	|t'::q' ->
-            match compare_mon (snd t) (snd t') with
-              1 -> t::(plusP p' q)
-            |(-1) -> t'::(plusP p q')
-            |_ -> let c=P.plusP (fst t) (fst t') in
-              match P.equal c coef0 with
-                true -> (plusP p' q')
-              |false -> (c,(snd t))::(plusP p' q')
-  in plusP p q
+  let rec plusP p q accu = match p, q with
+  | [], [] -> List.rev accu
+  | [], _ -> List.rev_append accu q
+  | _, [] -> List.rev_append accu p
+  | t :: p', t' :: q' ->
+    let c = compare_mon (snd t) (snd t') in
+    if c > 0 then plusP p' q (t :: accu)
+    else if c < 0 then plusP p q' (t' :: accu)
+    else
+      let c = P.plusP (fst t) (fst t') in
+      if P.equal c coef0 then plusP p' q' accu
+      else plusP p' q' ((c, (snd t)) :: accu)
+  in
+  plusP p q []
 
 (* multiplication by (a,monomial) *)
 let mult_t_pol a m p =
-  let rec mult_t_pol p =
-    match p with
-      [] -> []
-    |(b,m')::p -> ((P.multP a b),(mult_mon m m'))::(mult_t_pol p)
-  in mult_t_pol p
+  let map (b, m') = (P.multP a b, mult_mon m m') in
+  CList.map map p
 
 let coef_of_int x = P.of_num (Num.Int x)
 
@@ -451,23 +447,27 @@ let emultP a p =
   in emultP p
 
 let multP p q =
-  let rec aux p =
+  let rec aux p accu =
     match p with
-      [] -> []
-    |(a,m)::p' -> plusP (mult_t_pol a m q) (aux p')
-  in aux p
+      [] -> accu
+    |(a,m)::p' -> aux p' (plusP (mult_t_pol a m q) accu)
+  in aux p []
 
 let puisP p n=
   match p with
     [] -> []
   |_ ->
+    if n = 0 then
       let d = nvar (snd (List.hd p)) in
-      let rec puisP n =
-	match n with
-	  0 -> [coef1, Array.make (d+1) 0]
-	| 1 -> p
-	|_ -> multP p (puisP (n-1))
-      in puisP n
+      [coef1, Array.make (d+1) 0]
+    else
+      let rec puisP p n =
+        if n = 1 then p
+        else
+          let q = puisP p (n / 2) in
+          let q = multP q q in
+          if n mod 2 = 0 then q else multP p q
+      in puisP p n
 	
 let rec contentP p =
   match p with
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ad57c1643..72baa3493 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1870,16 +1870,22 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
 
 (* We put the tycon inside the arity signature, possibly discovering dependencies. *)
 
+let add_subst c len (rel_subst,var_subst) =
+  match kind_of_term c with
+  | Rel n -> (n,len) :: rel_subst, var_subst
+  | Var id -> rel_subst, (id,len) :: var_subst
+  | _ -> assert false
+
 let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
   let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
-  let subst, len =
+  let (rel_subst,var_subst), len =
     List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
       let signlen = List.length sign in
 	match kind_of_term tm with
-	  | Rel n when dependent tm c
+	  | Rel _ | Var _ when dependent tm c
 		&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
-	      ((n, len) :: subst, len - signlen)
-	  | Rel n when signlen > 1 (* The term is of a dependent type,
+	      (add_subst tm len subst, len - signlen)
+	  | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
 				      maybe some variable in its type appears in the tycon. *) ->
 	      (match tmtype with
 		  NotInd _ -> (subst, len - signlen)
@@ -1888,28 +1894,36 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
 		      List.fold_left
 			(fun (subst, len) arg ->
 			  match kind_of_term arg with
-			  | Rel n when dependent arg c ->
-			      ((n, len) :: subst, pred len)
+			  | Rel _ | Var _ when dependent arg c ->
+			      (add_subst arg len subst, pred len)
 			  | _ -> (subst, pred len))
 			(subst, len) realargs
 		    in
 		    let subst =
-		      if dependent tm c && List.for_all isRel realargs
-		      then (n, len) :: subst else subst
+		      if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
+		      then add_subst tm len subst else subst
 		    in (subst, pred len))
 	  | _ -> (subst, len - signlen))
-      (List.rev tomatchs) arsign ([], nar)
+      (List.rev tomatchs) arsign (([],[]), nar)
   in
   let rec predicate lift c =
     match kind_of_term c with
       | Rel n when n > lift ->
 	  (try
 	      (* Make the predicate dependent on the matched variable *)
-	      let idx = Int.List.assoc (n - lift) subst in
+	      let idx = Int.List.assoc (n - lift) rel_subst in
 		mkRel (idx + lift)
 	    with Not_found ->
-	      (* A variable that is not matched, lift over the arsign. *)
+	      (* A variable that is not matched, lift over the arsign *)
 	      mkRel (n + nar))
+      | Var id ->
+	  (try
+	      (* Make the predicate dependent on the matched variable *)
+	      let idx = Id.List.assoc id var_subst in
+		mkRel (idx + lift)
+	    with Not_found ->
+	      (* A variable that is not matched *)
+	      c)
       | _ ->
 	  map_constr_with_binders succ predicate lift c
   in
@@ -1925,46 +1939,44 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
  * type and 1 assumption for each term not _syntactically_ in an
  * inductive type.
 
- * Each matched terms are independently considered dependent or not.
-
- * A type constraint but no annotation case: we try to specialize the
- * tycon to make the predicate if it is not closed.
+ * Each matched term is independently considered dependent or not.
  *)
 
 let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
   let preds =
-    match pred, tycon with
+    match pred with
     (* No return clause *)
-    | None, Some t when not (noccur_with_meta 0 max_int t) ->
-	(* If the tycon is not closed w.r.t real variables, we try *)
-        (* two different strategies *)
-	(* First strategy: we abstract the tycon wrt to the dependencies *)
-        let p1 =
-          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
-	(* Second strategy: we build an "inversion" predicate *)
-	let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
-	(match p1 with
-	 | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
-	 | None -> [sigma2, pred2])
-    | None, _ ->
-	(* No dependent type constraint, or no constraints at all: *)
-	(* we use two strategies *)
-        let sigma,t = match tycon with
-	| Some t -> sigma,t
-	| None -> 
-          let sigma = Sigma.Unsafe.of_evar_map sigma in
-          let Sigma ((t, _), sigma, _) =
-	    new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
-          let sigma = Sigma.to_evar_map sigma in
-	    sigma, t
-	in
-        (* First strategy: we build an "inversion" predicate *)
+    | None ->
+        let sigma,t =
+          match tycon with
+          | Some t -> sigma, t
+          | None ->
+             (* No type constraint: we first create a generic evar type constraint *)
+             let src = (loc, Evar_kinds.CasesType false) in
+             let sigma = Sigma.Unsafe.of_evar_map sigma in
+             let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
+             let sigma = Sigma.to_evar_map sigma in
+             sigma, t in
+        (* First strategy: we build an "inversion" predicate, also replacing the *)
+        (* dependencies with existential variables *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
-	(* Second strategy: we directly use the evar as a non dependent pred *)
-        let pred2 = lift (List.length (List.flatten arsign)) t in
-	[sigma1, pred1; sigma, pred2]
+	(* Optional second strategy: we abstract the tycon wrt to the dependencies *)
+        let p2 =
+          prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
+        (* Third strategy: we take the type constraint as it is; of course we could *)
+        (* need something inbetween, abstracting some but not all of the dependencies *)
+        (* the "inversion" strategy deals with that but unification may not be *)
+        (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
+        (* work (yet) when a constructor has a type not precise enough for the inversion *)
+        (* see log message for details *)
+        let pred3 = lift (List.length (List.flatten arsign)) t in
+	(match p2 with
+	 | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) ->
+             [sigma1, pred1; sigma2, pred2; sigma, pred3]
+	 | _ ->
+             [sigma1, pred1; sigma, pred3])
     (* Some type annotation *)
-    | Some rtntyp, _ ->
+    | Some rtntyp ->
       (* We extract the signature of the arity *)
       let envar = List.fold_right push_rel_context arsign env in
       let sigma, newt = new_sort_variable univ_flexible_alg sigma in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 331ad0912..75159bf8b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -49,7 +49,11 @@ let invert_tag cst tag reloc_tbl =
   with Find_at j -> (j+1)
              (* Argggg, ces constructeurs de ... qui commencent a 1*)
 
-let find_rectype_a env c = Inductiveops.find_mrectype_vect env Evd.empty c
+let find_rectype_a env c =
+  let (t, l) = decompose_appvect (whd_all env c) in
+  match kind_of_term t with
+  | Ind ind -> (ind, l)
+  | _ -> assert false
 
 (* Instantiate inductives and parameters in constructor type *)
 
diff --git a/printing/printer.ml b/printing/printer.ml
index a6c7c5ca1..52cb07b8f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -735,9 +735,6 @@ let pr_prim_rule = function
       str(if Termops.occur_meta c then "refine " else "exact ") ++
       Constrextern.with_meta_as_hole pr_constr c
 
-  | Move (id1,id2) ->
-      (str"move "  ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
-
 (* Backwards compatibility *)
 
 let prterm = pr_lconstr
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5aba6b614..d23a4ad61 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -278,6 +278,11 @@ let move_hyp toleft (left,declfrom,right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
+let move_hyp_in_named_context hfrom hto sign =
+  let (left,right,declfrom,toleft) =
+    split_sign hfrom hto (named_context_of_val sign) in
+  move_hyp toleft (left,declfrom,right) hto
+
 (**********************************************************************)
 
 
@@ -552,12 +557,3 @@ let prim_refiner r sigma goal =
 	let sgl = List.rev sgl in
 	let sigma = Goal.V82.partial_solution sigma goal oterm in
 	  (sgl, sigma)
-
-    | Move (hfrom, hto) ->
-  	let (left,right,declfrom,toleft) =
-	  split_sign hfrom hto (named_context_of_val sign) in
-  	let hyps' =
-	  move_hyp toleft (left,declfrom,right) hto in
-	let (gl,ev,sigma) = mk_goal hyps' cl in
-	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
-  	  ([gl], sigma)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2764d28c0..0dba9ef1e 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -56,3 +56,6 @@ val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   Context.Named.Declaration.t -> Environ.named_context_val
+
+val move_hyp_in_named_context : Id.t -> Id.t Misctypes.move_location ->
+  Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index ff60ae5bf..03bc5e471 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -21,7 +21,6 @@ open Misctypes
 type prim_rule =
   | Cut of bool * bool * Id.t * types
   | Refine of constr
-  | Move of Id.t * Id.t move_location
 
 (** Nowadays, the only rules we'll consider are the primitive rules *)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 93e276f4b..904e22681 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -123,15 +123,11 @@ let internal_cut_rev_no_check replace id t gl =
 let refine_no_check c gl =
   refiner (Refine c) gl
 
-let move_hyp_no_check id1 id2 gl =
-  refiner (Move (id1,id2)) gl
-
 (* Versions with consistency checks *)
 
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
-let move_hyp id id'  = with_check (move_hyp_no_check id id')
 
 (* Pretty-printers *)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 100ed1522..727efcf6d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -92,7 +92,6 @@ val refine_no_check           : constr -> tactic
 val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic
-val move_hyp         : Id.t -> Id.t move_location -> tactic
 
 (** {6 Pretty-printing functions (debug only). } *)
 val pr_gls    : goal sigma -> Pp.std_ppcmds
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 49c91aa46..5d4350126 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -316,7 +316,18 @@ let apply_clear_request clear_flag dft c =
   else Tacticals.New.tclIDTAC
 
 (* Moving hypotheses *)
-let move_hyp id dest = Proofview.V82.tactic (Tacmach.move_hyp id dest)
+let move_hyp id dest =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let ty = Proofview.Goal.raw_concl gl in
+    let store = Proofview.Goal.extra gl in
+    let sign = named_context_val env in
+    let sign' = move_hyp_in_named_context id dest sign in
+    let env = reset_with_named_context sign' env in
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
+      Evarutil.new_evar env sigma ~principal:true ~store ty
+    end }
+  end }
 
 (* Renaming hypotheses *)
 let rename_hyp repl =
@@ -368,7 +379,7 @@ let rename_hyp repl =
       let nctx = Environ.val_of_named_context nhyps in
       let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
       Refine.refine ~unsafe:true { run = begin fun sigma ->
-        Evarutil.new_evar_instance nctx sigma nconcl ~store instance
+        Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
       end }
     end }
 
diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v
new file mode 100644
index 000000000..14af2d91d
--- /dev/null
+++ b/test-suite/bugs/closed/4785.v
@@ -0,0 +1,45 @@
+Require Coq.Lists.List Coq.Vectors.Vector.
+Require Coq.Compat.Coq85.
+
+Module A.
+Import Coq.Lists.List Coq.Vectors.Vector.
+Import ListNotations.
+Check [ ]%list : list _.
+Import VectorNotations ListNotations.
+Delimit Scope vector_scope with vector.
+Check [ ]%vector : Vector.t _ _.
+Check []%vector : Vector.t _ _.
+Check [ ]%list : list _.
+Check []%list : list _.
+
+Goal True.
+  idtac; []. (* Check that vector notations don't break the [ | .. | ] syntax of Ltac *)
+Abort.
+
+Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
+Delimit Scope mylist_scope with mylist.
+Bind Scope mylist_scope with mylist.
+Arguments mynil {_}, _.
+Arguments mycons {_} _ _.
+Notation " [] " := mynil : mylist_scope.
+Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
+Notation " [ x ] " := (mycons x nil) : mylist_scope.
+Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
+
+Import Coq.Compat.Coq85.
+Locate Module VectorNotations.
+Import VectorDef.VectorNotations.
+
+Check []%vector : Vector.t _ _.
+Check []%mylist : mylist _.
+Check [ ]%mylist : mylist _.
+Check [ ]%list : list _.
+End A.
+
+Module B.
+Import Coq.Compat.Coq85.
+
+Goal True.
+  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
+Abort.
+End B.
diff --git a/test-suite/bugs/closed/5093.v b/test-suite/bugs/closed/5093.v
new file mode 100644
index 000000000..3ded4dd30
--- /dev/null
+++ b/test-suite/bugs/closed/5093.v
@@ -0,0 +1,11 @@
+Axiom P : nat -> Prop.
+Axiom PS : forall n, P n -> P (S n).
+Axiom P0 : P 0.
+
+Hint Resolve PS : foobar.
+Hint Resolve P0 : foobar.
+
+Goal P 100.
+Proof.
+Fail typeclasses eauto 100 with foobar.
+typeclasses eauto 101 with foobar.
diff --git a/test-suite/bugs/closed/5096.v b/test-suite/bugs/closed/5096.v
new file mode 100644
index 000000000..20a537ab3
--- /dev/null
+++ b/test-suite/bugs/closed/5096.v
@@ -0,0 +1,219 @@
+Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos Coq.Lists.List.
+
+Set Asymmetric Patterns.
+
+Notation eta x := (fst x, snd x).
+
+Inductive expr {var : Type} : Type :=
+| Const : expr
+| LetIn : expr -> (var -> expr) -> expr.
+
+Definition Expr := forall var, @expr var.
+
+Fixpoint count_binders (e : @expr unit) : nat :=
+match e with
+| LetIn _ eC => 1 + @count_binders (eC tt)
+| _ => 0
+end.
+
+Definition CountBinders (e : Expr) : nat := count_binders (e _).
+
+Class Context (Name : Type) (var : Type) :=
+  { ContextT : Type;
+    extendb : ContextT -> Name -> var -> ContextT;
+    empty : ContextT }.
+Coercion ContextT : Context >-> Sortclass.
+Arguments ContextT {_ _ _}, {_ _} _.
+Arguments extendb {_ _ _} _ _ _.
+Arguments empty {_ _ _}.
+
+Module Export Named.
+Inductive expr Name : Type :=
+| Const : expr Name
+| LetIn : Name -> expr Name -> expr Name -> expr Name.
+End Named.
+
+Global Arguments Const {_}.
+Global Arguments LetIn {_} _ _ _.
+
+Definition split_onames {Name : Type} (ls : list (option Name))
+  : option (Name) * list (option Name)
+  := match ls with
+          | cons n ls'
+            => (n, ls')
+          | nil => (None, nil)
+     end.
+
+Section internal.
+  Context (InName OutName : Type)
+          {InContext : Context InName (OutName)}
+          {ReverseContext : Context OutName (InName)}
+          (InName_beq : InName -> InName -> bool).
+
+  Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext)
+           (e : expr InName) (new_names : list (option OutName))
+    : option (expr OutName)
+    := match e in Named.expr _ return option (expr _) with
+       | Const => Some Const
+       | LetIn n ex eC
+         => let '(n', new_names') := eta (split_onames new_names) in
+            match n', @register_reassign ctxi ctxr ex nil with
+            | Some n', Some x
+              => let ctxi := @extendb _ _ _ ctxi n n' in
+                 let ctxr := @extendb _ _ _ ctxr n' n in
+                 option_map (LetIn n' x) (@register_reassign ctxi ctxr eC new_names')
+            | None, Some x
+              => let ctxi := ctxi in
+                 @register_reassign ctxi ctxr eC new_names'
+            | _, None => None
+            end
+       end.
+
+End internal.
+
+Global Instance pos_context (var : Type) : Context positive var
+  := { ContextT := PositiveMap.t var;
+       extendb ctx key v := PositiveMap.add key v ctx;
+       empty := PositiveMap.empty _ }.
+
+Global Arguments register_reassign {_ _ _ _} ctxi ctxr e _.
+
+Section language5.
+  Context (Name : Type).
+
+  Local Notation expr := (@Top.expr Name).
+  Local Notation nexpr := (@Named.expr Name).
+
+  Fixpoint ocompile (e : expr) (ls : list (option Name)) {struct e}
+    : option (nexpr)
+    := match e in @Top.expr _ return option (nexpr) with
+       | Top.Const => Some Named.Const
+       | Top.LetIn ex eC
+         => match @ocompile ex nil, split_onames ls with
+            | Some x, (Some n, ls')%core
+              => option_map (fun C => Named.LetIn n x C) (@ocompile (eC n) ls')
+            | _, _ => None
+            end
+       end.
+
+  Definition compile (e : expr) (ls : list Name) := @ocompile e (List.map (@Some _) ls).
+End language5.
+
+Global Arguments compile {_} e ls.
+
+Fixpoint merge_liveness (ls1 ls2 : list unit) :=
+  match ls1, ls2 with
+  | cons x xs, cons y ys => cons tt (@merge_liveness xs ys)
+  | nil, ls | ls, nil => ls
+  end.
+
+Section internal1.
+  Context (Name : Type)
+          (OutName : Type)
+          {Context : Context Name (list unit)}.
+
+  Definition compute_livenessf_step
+             (compute_livenessf : forall (ctx : Context) (e : expr Name) (prefix : list unit), list unit)
+             (ctx : Context)
+             (e : expr Name) (prefix : list unit)
+    : list unit
+    := match e with
+       | Const => prefix
+       | LetIn n ex eC
+         => let lx := @compute_livenessf ctx ex prefix in
+            let lx := merge_liveness lx (prefix ++ repeat tt 1) in
+            let ctx := @extendb _ _ _ ctx n (lx) in
+            @compute_livenessf ctx eC (prefix ++ repeat tt 1)
+       end.
+
+  Fixpoint compute_liveness ctx e prefix
+    := @compute_livenessf_step (@compute_liveness) ctx e prefix.
+
+  Fixpoint insert_dead_names_gen def (ls : list unit) (lsn : list OutName)
+    : list (option OutName)
+    := match ls with
+       | nil => nil
+       | cons live xs
+         => match lsn with
+            | cons n lsn' => Some n :: @insert_dead_names_gen def xs lsn'
+            | nil => def :: @insert_dead_names_gen def xs nil
+            end
+       end.
+  Definition insert_dead_names def (e : expr Name)
+    := insert_dead_names_gen def (compute_liveness empty e nil).
+End internal1.
+
+Global Arguments insert_dead_names {_ _ _} def e lsn.
+
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
+
+Section language7.
+  Context {Context : Context unit (positive)}.
+
+  Local Notation nexpr := (@Named.expr unit).
+
+  Definition CompileAndEliminateDeadCode (e : Expr) (ls : list unit)
+    : option (nexpr)
+    := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in
+       match e with
+       | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *)
+                          (fun names => register_reassign empty empty e names)
+       | None => None
+       end.
+End language7.
+
+Global Arguments CompileAndEliminateDeadCode {_} e ls.
+
+Definition ContextOn {Name1 Name2} f {var} (Ctx : Context Name1 var) : Context Name2 var
+  := {| ContextT := Ctx;
+        extendb ctx n v := extendb ctx (f n) v;
+        empty := empty |}.
+
+Definition Register := Datatypes.unit.
+
+Global Instance RegisterContext {var : Type} : Context Register var
+  := ContextOn (fun _ => 1%positive) (pos_context var).
+
+Definition syntax := Named.expr Register.
+
+Definition AssembleSyntax e ls (res := CompileAndEliminateDeadCode e ls)
+  := match res return match res with None => _ | _ => _ end with
+     | Some v => v
+     | None => I
+     end.
+
+Definition dummy_registers (n : nat) : list Register
+  := List.map (fun _ => tt) (seq 0 n).
+Definition DefaultRegisters (e : Expr) : list Register
+  := dummy_registers (CountBinders e).
+
+Definition DefaultAssembleSyntax e := @AssembleSyntax e (DefaultRegisters e).
+
+Notation "'slet' x := A 'in' b" := (Top.LetIn A (fun x => b)) (at level 200, b at level 200).
+Notation "#[ var ]#" := (@Top.Const var).
+
+Definition compiled_syntax : Expr := fun (var : Type) =>
+(
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+  slet x1 := #[ var ]# in
+ @Top.Const var).
+
+Definition v :=
+  Eval cbv [compiled_syntax] in (DefaultAssembleSyntax (compiled_syntax)).
+
+Timeout 2 Eval vm_compute in v.
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v
index 8f95484cf..356a67efe 100644
--- a/test-suite/success/Case13.v
+++ b/test-suite/success/Case13.v
@@ -87,3 +87,41 @@ Check fun (x : E) => match x with c => e c end.
 Inductive C' : bool -> Set := c' : C' true.
 Inductive E' (b : bool) : Set := e' :> C' b -> E' b.
 Check fun (x : E' true) => match x with c' => e' true c' end.
+
+(* Check use of the no-dependency strategy when a type constraint is
+   given (and when the "inversion-and-dependencies-as-evars" strategy
+   is not strong enough because of a constructor with a type whose
+   pattern structure is not refined enough for it to be captured by
+   the inversion predicate) *)
+
+Inductive K : bool -> bool -> Type := F : K true true | G x : K x x.
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y, P y -> Q y z) =>
+        match y with
+        | F  => f y H1
+        | G _ => f y H2
+        end : Q y z.
+
+(* Check use of the maximal-dependency-in-variable strategy even when
+   no explicit type constraint is given (and when the
+   "inversion-and-dependencies-as-evars" strategy is not strong enough
+   because of a constructor with a type whose pattern structure is not
+   refined enough for it to be captured by the inversion predicate) *)
+
+Check fun z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z) =>
+        match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end.
+
+(* Check use of the maximal-dependency-in-variable strategy for "Var"
+   variables *)
+
+Goal forall z P Q (y:K true z) (H1 H2:P y) (f:forall y z, P y -> Q y z), Q y z.
+intros z P Q y H1 H2 f.
+Show.
+refine (match y with
+        | F  => f y true H1
+        | G b => f y b H2
+        end).
+Qed.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 341be92d1..5eecdc64c 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -77,8 +77,8 @@ Coercion sig2_of_sigT2 : sigT2 >-> sig2.
 (** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5.  This is necessary.  These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *)
 Require Coq.Lists.List.
 Require Coq.Vectors.VectorDef.
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
-Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
+Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) : list_scope.
+Notation "[ x ; .. ; y ]" := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope.
 
 (** In 8.4, the statement of admitted lemmas did not depend on the section
     variables. *)
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 0ddf1acde..54aeeaa11 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -21,4 +21,22 @@ Global Unset Regular Subst Tactic.
 Global Unset Structural Injection.
 Global Unset Shrink Abstract.
 Global Unset Shrink Obligations.
-Global Set Refolding Reduction.
\ No newline at end of file
+Global Set Refolding Reduction.
+
+(** In Coq 8.5, [] meant Vector, and [ ] meant list.  Restore this
+    behavior, to allow user-defined [] to not override vector
+    notations.  See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *)
+
+Require Coq.Lists.List.
+Require Coq.Vectors.VectorDef.
+Module Export Coq.
+Module Export Vectors.
+Module VectorDef.
+Export Coq.Vectors.VectorDef.
+Module VectorNotations.
+Export Coq.Vectors.VectorDef.VectorNotations.
+Notation "[]" := (VectorDef.nil _) : vector_scope.
+End VectorNotations.
+End VectorDef.
+End Vectors.
+End Coq.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 9886ae6a8..fc94d7e25 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -21,12 +21,12 @@ Set Implicit Arguments.
 
 Open Scope list_scope.
 
-(** Standard notations for lists. 
+(** Standard notations for lists.
 In a special module to avoid conflicts. *)
 Module ListNotations.
-Notation " [ ] " := nil (format "[ ]") : list_scope.
-Notation " [ x ] " := (cons x nil) : list_scope.
-Notation " [ x ; y ; .. ; z ] " :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
+Notation "[ ]" := nil (format "[ ]") : list_scope.
+Notation "[ x ]" := (cons x nil) : list_scope.
+Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
 End ListNotations.
 
 Import ListNotations.
@@ -195,7 +195,7 @@ Section Facts.
   Qed.
 
   Theorem app_nil_r : forall l:list A, l ++ [] = l.
-  Proof. 
+  Proof.
     induction l; simpl; f_equal; auto.
   Qed.
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index c69223804..f49b34075 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -30,7 +30,7 @@ Inductive t A : nat -> Type :=
   |nil : t A 0
   |cons : forall (h:A) (n:nat), t A n -> t A (S n).
 
-Local Notation "[]" := (nil _).
+Local Notation "[ ]" := (nil _) (format "[ ]").
 Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).
 
 Section SCHEMES.
@@ -102,7 +102,7 @@ Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
 
 Computational behavior of this function should be the same as
 ocaml function. *)
-Definition nth {A} := 
+Definition nth {A} :=
 fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
 match p in Fin.t m' return t A m' -> A with
  |Fin.F1 => caseS (fun n v' => A) (fun h n t => h)
@@ -293,11 +293,12 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni
 End VECTORLIST.
 
 Module VectorNotations.
-Notation "[]" := [] : vector_scope.
+Delimit Scope vector_scope with vector.
+Notation "[ ]" := [] (format "[ ]") : vector_scope.
 Notation "h :: t" := (h :: t) (at level 60, right associativity)
   : vector_scope.
-Notation " [ x ] " := (x :: []) : vector_scope.
-Notation " [ x ; y ; .. ; z ] " := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
+Notation "[ x ]" := (x :: []) : vector_scope.
+Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope
 .
 Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
 Open Scope vector_scope.
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7ff59c471..35645c8e7 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -108,7 +108,7 @@ let init_load_path () =
     (* additional loadpath, given with options -Q and -R *)
     List.iter
       (fun (unix_path, coq_root, implicit) ->
-        Mltop.add_rec_path Mltop.AddTopML ~unix_path ~coq_root ~implicit)
+        Mltop.add_rec_path Mltop.AddNoML ~unix_path ~coq_root ~implicit)
       (List.rev !includes);
     (* additional ml directories, given with option -I *)
     List.iter Mltop.add_ml_dir (List.rev !ml_includes)