diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-22 15:39:28 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-28 02:33:43 +0100 |
| commit | 9af1d5ae4dbed8557b5c715a65f2742c57641f52 (patch) | |
| tree | dac7e73c397edb30ffdd4e076d4efe792a8464bc /grammar | |
| parent | cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 (diff) | |
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.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 23 |
1 files changed, 14 insertions, 9 deletions
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 |