diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-12-16 18:35:34 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-02-07 17:38:00 +0100 |
| commit | 5e909ab948ea3db4b5d734ec1c68198874c9724c (patch) | |
| tree | 7995019027ddaa7e96cb65e7b7cdec2d0354ebd4 | |
| parent | d8e918e48048b09f859421861ba0bf487e5a0d48 (diff) | |
pre_ident can be bound to Ltac variables.
The use case is to take a hint database as an argument of Ltac or Tactic Notation.
| -rw-r--r-- | ltac/tacintern.ml | 1 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 7 | ||||
| -rw-r--r-- | ltac/tacsubst.ml | 1 |
3 files changed, 6 insertions, 3 deletions
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 763e0dc22..4b5d87fc3 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -782,6 +782,7 @@ let intern_ltac ist tac = let () = Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var); Genintern.register_intern0 wit_ref (lift intern_global_reference); + Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c)); Genintern.register_intern0 wit_ident intern_ident'; Genintern.register_intern0 wit_var (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 32bcdfb6a..fda9142ed 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -2023,9 +2023,6 @@ let () = let () = declare_uniform wit_string -let () = - declare_uniform wit_pre_ident - let lift f = (); fun ist x -> Ftactic.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in @@ -2053,9 +2050,13 @@ let interp_destruction_arg' ist c = Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (interp_destruction_arg ist gl c) end } +let interp_pre_ident ist env sigma s = + s |> Id.of_string |> interp_ident ist env sigma |> Id.to_string + let () = register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n)); register_interp0 wit_ref (lift interp_reference); + register_interp0 wit_pre_ident (lift interp_pre_ident); register_interp0 wit_ident (lift interp_ident); register_interp0 wit_var (lift interp_hyp); register_interp0 wit_intro_pattern (lifts interp_intro_pattern); diff --git a/ltac/tacsubst.ml b/ltac/tacsubst.ml index 55de58361..b09bdda65 100644 --- a/ltac/tacsubst.ml +++ b/ltac/tacsubst.ml @@ -291,6 +291,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) = let () = Genintern.register_subst0 wit_int_or_var (fun _ v -> v); Genintern.register_subst0 wit_ref subst_global_reference; + Genintern.register_subst0 wit_pre_ident (fun _ v -> v); Genintern.register_subst0 wit_ident (fun _ v -> v); Genintern.register_subst0 wit_var (fun _ v -> v); Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); |