6 files changed, 23 insertions, 25 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 21d61d1f97..f7215a9d13 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1100,7 +1100,7 @@ VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
-| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) }
+| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_notice (Keys.pr_keys Printer.pr_global) }
 END
 
 
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 455c8ab003..61cc77c42a 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -145,7 +145,7 @@ open Pp
 
 VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
 | [ "Show" "Obligation" "Tactic" ] -> {
-    Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) }
+    Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
 END
 
 VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
@@ -154,8 +154,8 @@ VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY
 END
 
 VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY
-| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) }
-| [ "Preterm" ] -> { Feedback.msg_info (show_term None) }
+| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_notice (show_term (Some name)) }
+| [ "Preterm" ] -> { Feedback.msg_notice (show_term None) }
 END
 
 {
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 9d46bbc74e..fe5ebf1172 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -417,7 +417,7 @@ let get_timer name =
 let finish_timing ~prefix name =
   let tend = System.get_time () in
   let tstart = get_timer name in
-  Feedback.msg_info(str prefix ++ pr_opt str name ++ str " ran for " ++
+  Feedback.msg_notice(str prefix ++ pr_opt str name ++ str " ran for " ++
                     System.fmt_time_difference tstart tend)
 
 (* ******************** *)
@@ -431,7 +431,7 @@ let print_results_filter ~cutoff ~filter =
   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_info (to_string ~cutoff ~filter results)
+  Feedback.msg_notice (to_string ~cutoff ~filter results)
 ;;
 
 let print_results ~cutoff =
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 9e8e86d4fc..252c15478d 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -20,7 +20,7 @@ let make0 ?dyn name =
   wit
 
 let wit_intropattern = make0 "intropattern" (* To keep after deprecation phase but it will get a different parsing semantics (Tactic Notation and TACTIC EXTEND) in pltac.ml *)
-let wit_simple_intropattern = make0 "simple_intropattern"
+let wit_simple_intropattern = make0 ~dyn:(val_tag (topwit wit_intropattern)) "simple_intropattern"
 let wit_quant_hyp = make0 "quant_hyp"
 let wit_constr_with_bindings = make0 "constr_with_bindings"
 let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index e64129d204..da89a027e2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -145,11 +145,8 @@ let coerce_to_constr_context v =
   else raise (CannotCoerceTo "a term context")
 
 let is_intro_pattern v =
-  if has_type v (topwit wit_intropattern [@warning "-3"]) then
-    Some (out_gen (topwit wit_intropattern [@warning "-3"]) v).CAst.v
-  else
-  if has_type v (topwit wit_simple_intropattern) then
-    Some (out_gen (topwit wit_simple_intropattern) v).CAst.v
+  if has_type v (topwit wit_intro_pattern) then
+    Some (out_gen (topwit wit_intro_pattern) v).CAst.v
   else
     None
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 94af4a3151..ba759441e5 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -189,31 +189,32 @@ let flatten_contravariant_disj _ ist =
       tclTHEN (tclTHENLIST tacs) tac0
   | _ -> fail
 
-let make_unfold name =
-  let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in
-  let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in
-  Locus.(AllOccurrences, ArgArg (EvalConstRef const, None))
+let evalglobref_of_globref =
+  function
+  | GlobRef.VarRef v -> EvalVarRef v
+  | GlobRef.ConstRef c -> EvalConstRef c
+  | GlobRef.IndRef _ | GlobRef.ConstructRef _ -> assert false
 
-let u_not = make_unfold "not"
+let make_unfold name =
+  let const = evalglobref_of_globref (Coqlib.lib_ref name) in
+  Locus.(AllOccurrences, ArgArg (const, None))
 
 let reduction_not_iff _ ist =
   let make_reduce c = TacAtom (CAst.make @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
   let tac = match !negation_unfolding with
-    | true -> make_reduce [u_not]
+    | true -> make_reduce [make_unfold "core.not.type"]
     | false -> TacId []
   in
   eval_tactic_ist ist tac
 
-let coq_nnpp_path =
-  let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in
-  Libnames.make_path (DirPath.make dir) (Id.of_string "NNPP")
-
 let apply_nnpp _ ist =
+  let nnpp = "core.nnpp.type" in
   Proofview.tclBIND
     (Proofview.tclUNIT ())
-    begin fun () -> try
-      Tacticals.New.pf_constr_of_global (Nametab.global_of_path coq_nnpp_path) >>= apply
-    with Not_found -> tclFAIL 0 (Pp.mt ())
+    begin fun () ->
+      if Coqlib.has_ref nnpp
+      then Tacticals.New.pf_constr_of_global (Coqlib.lib_ref nnpp) >>= apply
+      else tclFAIL 0 (Pp.mt ())
     end
 
 (* This is the uniform mode dealing with ->, not, iff and types isomorphic to