Revert "[with_strategy] Fix for coqchk"

This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18.

We instead add a warning in the manual and a kludge in the test-suite.

3 files changed, 15 insertions, 13 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7483ab3341..bc2168411b 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3467,6 +3467,16 @@ the conversion in hypotheses :n:`{+ @ident}`.
       :tacn:`with_strategy` may not be robustly performant when
       scaling the size of the input.
 
+   .. warning::
+
+      In much the same way this tactic does not play well with
+      :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as
+      an intermediary, this tactic does not play well with ``coqchk``,
+      even when used with :tacn:`abstract`, due to the inability of
+      tactics to persist information about conversion hints in the
+      proof term. See `#12200
+      <https://github.com/coq/coq/issues/12200>`_ for more details.
+
 Conversion tactics applied to hypotheses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 42c389aa58..c1b1076102 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5084,13 +5084,6 @@ let with_set_strategy lvl_ql k =
     | GlobRef.VarRef id -> VarKey id
     | _ -> user_err Pp.(str
                           "cannot set an inductive type or a constructor as transparent") in
-  let eval_glob_ref_of_key r =
-    match r with
-    | ConstKey sp -> EvalConstRef sp
-    | VarKey id -> EvalVarRef id
-    | _ -> user_err Pp.(str
-                          "cannot set an inductive type or a constructor as transparent") in
-  let local = true in
   let kl = List.concat (List.map (fun (lvl, ql) -> List.map (fun q -> (lvl, glob_key q)) ql) lvl_ql) in
   tclWRAPFINALLY
     (Proofview.tclENV >>= fun env ->
@@ -5110,18 +5103,14 @@ let with_set_strategy lvl_ql k =
            (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in
      Proofview.Unsafe.tclSETENV env <*>
      Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
-         List.iter (fun (lvl, k) -> Global.set_strategy k lvl;
-                     Redexpr.set_strategy local [(lvl, [eval_glob_ref_of_key k])])
-           kl)) <*>
+         List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl)) <*>
      Proofview.tclUNIT (orig_kl, orig_kl_global))
     k
     (fun (orig_kl, orig_kl_global) ->
        (* TODO: When abstract no longer depends on Global, remove this
           [Proofview.tclLIFT] block *)
        Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
-           List.iter (fun (lvl, k) -> Global.set_strategy k lvl;
-                       Redexpr.set_strategy local [(lvl, [eval_glob_ref_of_key k])])
-             orig_kl_global)) <*>
+           List.iter (fun (lvl, k) -> Global.set_strategy k lvl) orig_kl_global)) <*>
        Proofview.tclENV >>= fun env ->
        let env = List.fold_left (fun env (lvl, k) ->
            Environ.set_oracle env
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index e0d0252a47..077b57c87f 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -572,3 +572,6 @@ Goal id 0 = 0.
                                    (assert_succeeds unfold_id))))))))))).
   reflexivity.
 Qed.
+
+(* Fake out coqchk to work around what is essentially COQBUG(https://github.com/coq/coq/issues/12200) *)
+Reset Initial.