Deprecating Cd in favor of -output-directory or Set Extraction Output…

… Directory.

New attempt to Alizter's PR coq#16119.

doc/sphinx/addendum/extraction.rst

@@ -103,6 +103,12 @@ in the Coq sources.
 
 .. cmd:: Cd {? @string }
 
+   .. deprecated:: 8.20
+
+      Use instead the command line option :n:`-output-directory` (see
+      :ref:`command-line-options`), or the :flag:`Extraction Output Directory`
+      option.
+
    If :n:`@string` is specified, changes the current directory according to
    :token:`string` which can be any valid path.  Otherwise, it displays the
    current directory as :cmd:`Pwd` does.

vernac/synterp.ml

@@ -318,9 +318,14 @@ let synterp_declare_ml_module ~local l =
   let l = List.map expand l in
   Mltop.declare_ml_modules local l
 
+let warn_chdir = CWarnings.create ~name:"change-dir-deprecated" ~category:Deprecation.Version.v8_18
+    (fun () -> strbrk "Command \"Cd\" is deprecated." ++ spc () ++
+               strbrk "Use command-line \"-output-directory dir\" instead.")
+
 let synterp_chdir = function
   | None -> Feedback.msg_notice (str (Sys.getcwd()))
   | Some path ->
+      warn_chdir ();
       begin
         try Sys.chdir (expand path)
         with Sys_error err ->