diff options
Diffstat (limited to 'tactics/ftactic.ml')
| -rw-r--r-- | tactics/ftactic.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml index 6d6e43b21d..01c2fde2a9 100644 --- a/tactics/ftactic.ml +++ b/tactics/ftactic.ml @@ -48,6 +48,15 @@ let enter f = bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)) (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) +let with_env t = + t >>= function + | Uniform a -> + Proofview.tclENV >>= fun env -> Proofview.tclUNIT (Uniform (env,a)) + | Depends l -> + Proofview.Goal.goals >>= fun gs -> + Proofview.Monad.(List.map (map Proofview.Goal.env) gs) >>= fun envs -> + Proofview.tclUNIT (Depends (List.combine envs l)) + let lift (type a) (t:a Proofview.tactic) : a t = Proofview.tclBIND t (fun x -> Proofview.tclUNIT (Uniform x)) |