[with_strategy] Fix for coqchk

We need to record the transparency information in the libobject stack in
order for coqchk to not trip over the strategy information.

This is quite sketchy, though.

1 files changed, 13 insertions, 2 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c1b1076102..42c389aa58 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5084,6 +5084,13 @@ 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 ->
@@ -5103,14 +5110,18 @@ 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) kl)) <*>
+         List.iter (fun (lvl, k) -> Global.set_strategy k lvl;
+                     Redexpr.set_strategy local [(lvl, [eval_glob_ref_of_key k])])
+           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) orig_kl_global)) <*>
+           List.iter (fun (lvl, k) -> Global.set_strategy k lvl;
+                       Redexpr.set_strategy local [(lvl, [eval_glob_ref_of_key k])])
+             orig_kl_global)) <*>
        Proofview.tclENV >>= fun env ->
        let env = List.fold_left (fun env (lvl, k) ->
            Environ.set_oracle env