From 9af1d5ae4dbed8557b5c715a65f2742c57641f52 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 22 Dec 2015 15:39:28 +0100 Subject: Implementing non-focussed generic arguments. Kind of enhances the situation of bug #4409. Now arguments can be interpreted globally or focussedly in a dynamic fashion because the interpretation function returns a Ftactic.t. The bug is not fixed yet because we should tweak the interpretation of tactic arguments. --- grammar/argextend.ml4 | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) (limited to 'grammar/argextend.ml4') diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index f6c223b74..677daebfb 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -182,17 +182,22 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = | None -> begin match globtyp with | Genarg.ExtraArgType s' when CString.equal s s' -> - <:expr< fun ist gl v -> (gl.Evd.sigma, v) >> + <:expr< fun ist v -> Ftactic.return v >> | _ -> - <:expr< fun ist gl x -> - let (sigma,a_interp) = - Tacinterp.interp_genarg ist - (Tacmach.pf_env gl) (Tacmach.project gl) (Tacmach.pf_concl gl) gl.Evd.it - (Genarg.in_gen $make_globwit loc globtyp$ x) - in - (sigma , Tacinterp.Value.cast $make_topwit loc globtyp$ a_interp)>> + <:expr< fun ist x -> + Ftactic.bind + (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x)) + (fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >> end - | Some f -> <:expr< $lid:f$>> in + | Some f -> + (** Compatibility layer, TODO: remove me *) + <:expr< + let f = $lid:f$ in + fun ist v -> Ftactic.nf_enter (fun gl -> + let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in + Ftactic.bind (Ftactic.lift (Proofview.Unsafe.tclEVARS sigma)) (fun _ -> Ftactic.return v) + ) + >> in let subst = match h with | None -> begin match globtyp with -- cgit v1.2.3