aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorJason Gross2020-05-09 13:39:34 -0400
committerJason Gross2020-05-09 13:39:34 -0400
commit6b223d1d668ecb76aa2609b7d6bb8a19e13136cd (patch)
tree8e67bb69a5b1bf7371c9e80adb75096e0077b03d /tactics
parent3c66c60e52b334482bcfe3d1d97bb77e4d011d18 (diff)
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.
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tactics.ml15
1 files changed, 2 insertions, 13 deletions
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