Merge PR coq#15277: Deprecate the argument-free instantiate tactic

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

doc/changelog/04-tactics/15277-deprecate-instantiate-tactic.rst

@@ -0,0 +1,5 @@
+- **Deprecated:**
+  the :tacn:`instantiate` tactic without arguments. Since the move to
+  the monadic tactic engine in 8.5, it was behaving as the identity
+  (`#15277 <https://github.com/coq/coq/pull/15277>`_,
+  by Pierre-Marie Pédrot).

doc/sphinx/proof-engine/tactics.rst

@@ -1607,11 +1607,9 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`.
 
 .. tacv:: instantiate
 
-   Without argument, the instantiate tactic tries to solve as many existential
-   variables as possible, using information gathered from other tactics in the
-   same tactical. This is automatically done after each complete tactic (i.e.
-   after a dot in proof mode), but not, for example, between each tactic when
-   they are sequenced by semicolons.
+   This tactic behaves functionally as :tacn:`idtac`.
+
+   .. deprecated:: 8.16
 
 .. tacn:: admit
    :name: admit

engine/proofview.ml

@@ -1231,17 +1231,6 @@ module V82 = struct
       let (e, info) = Exninfo.capture e in
       tclZERO ~info e
 
-
-  (* normalises the evars in the goals, and stores the result in
-     solution. *)
-  let nf_evar_goals =
-    Pv.modify begin fun ps ->
-    let map g s = goal_nf_evar s g in
-    let comb = CList.map drop_state ps.comb in
-    let (_goals,evd) = Evd.Monad.List.map map comb ps.solution in
-    { ps with solution = evd; }
-    end
-
   let top_goals initial { solution=solution; } =
     let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
     { Evd.it = goals ; sigma=solution; }

engine/proofview.mli

@@ -595,10 +595,6 @@ module V82 : sig
    * (conclusion and context) before calling the tactic *)
   val tactic : ?nf_evars:bool -> tac -> unit tactic
 
-  (* normalises the evars in the goals, and stores the result in
-     solution. *)
-  val nf_evar_goals : unit tactic
-
   val top_goals : entry -> proofview -> Evar.t list Evd.sigma
 
   (* returns the existential variable used to start the proof *)

plugins/ltac/extratactics.mlg

@@ -368,10 +368,13 @@ END
 
 TACTIC EXTEND instantiate
 | [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] ->
-    { Tacticals.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals }
+    { instantiate_tac_by_name id c }
 | [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] ->
-    { Tacticals.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals }
-| [ "instantiate" ] -> { Proofview.V82.nf_evar_goals }
+    { instantiate_tac i c hl }
+END
+
+TACTIC EXTEND instantiate_noarg DEPRECATED { Deprecation.make ~since:"8.16" () }
+| [ "instantiate" ] -> { Proofview.tclUNIT () }
 END
 
 (**********************************************************************)