diff options
| author | Jason Gross | 2020-05-09 13:39:34 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 13:39:34 -0400 |
| commit | 6b223d1d668ecb76aa2609b7d6bb8a19e13136cd (patch) | |
| tree | 8e67bb69a5b1bf7371c9e80adb75096e0077b03d /tactics | |
| parent | 3c66c60e52b334482bcfe3d1d97bb77e4d011d18 (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.ml | 15 |
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 |
