diff options
| -rw-r--r-- | tactics/ftactic.ml | 9 | ||||
| -rw-r--r-- | tactics/ftactic.mli | 5 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 22 |
3 files changed, 30 insertions, 6 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)) diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli index 19ef717bc9..3102869ef9 100644 --- a/tactics/ftactic.mli +++ b/tactics/ftactic.mli @@ -44,6 +44,11 @@ val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is focussed. *) +val with_env : 'a t -> (Environ.env*'a) t +(** [with_env t] returns, in addition to the return type of [t], an + environment, which is the global environment if [t] does not focus on + goals, or the local goal environment if [t] focuses on goals. *) + (** {5 Notations} *) val (>>=) : 'a t -> ('a -> 'b t) -> 'b t diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a726253dc8..c0dac416cd 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1217,18 +1217,28 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with end in let (>>=) = Ftactic.bind in - let addvar (x, v) accu = - f v >>= fun v -> - Ftactic.return (Id.Map.add x v accu) + let interp_vars = + Ftactic.List.map (fun (x,v) -> f v >>= fun v -> Ftactic.return (x,v)) l in - let tac = Ftactic.List.fold_right addvar l ist.lfun >>= fun lfun -> + let addvar (x, v) accu = Id.Map.add x v accu in + let tac l = + let lfun = List.fold_right addvar l ist.lfun in let trace = push_trace (loc,LtacNotationCall s) ist in let ist = { lfun = lfun; extra = TacStore.set ist.extra f_trace trace; } in - val_interp ist body + val_interp ist body >>= fun v -> + Ftactic.lift (tactic_of_value ist v) in - Ftactic.run tac (fun v -> tactic_of_value ist v) + let tac = + Ftactic.with_env interp_vars >>= fun (env,l) -> + let name () = Pptactic.pr_tactic env (TacAlias(loc,s,l)) in + Proofview.Trace.name_tactic name (tac l) + (* spiwack: this use of name_tactic is not robust to a + change of implementation of [Ftactic]. In such a situation, + some more elaborate solution will have to be used. *) + in + Ftactic.run tac (fun () -> Proofview.tclUNIT ()) | TacML (loc,opn,l) when List.for_all global_genarg l -> let trace = push_trace (loc,LtacMLCall tac) ist in |