diff options
Diffstat (limited to 'ltac/tacintern.ml')
| -rw-r--r-- | ltac/tacintern.ml | 20 |
1 files changed, 4 insertions, 16 deletions
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index b6ff32ac3..f51cc3518 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -775,13 +775,16 @@ let intern_ident' ist id = let lf = ref Id.Set.empty in (ist, intern_ident lf ist id) +let intern_ltac ist tac = + Flags.with_option strict_check (fun () -> intern_pure_tactic 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_ident intern_ident'; Genintern.register_intern0 wit_var (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); - Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg); + Genintern.register_intern0 wit_ltac (lift intern_ltac); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c)); Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)); @@ -791,18 +794,3 @@ let () = Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings); Genintern.register_intern0 wit_destruction_arg (lift intern_destruction_arg); () - -(***************************************************************************) -(* Backwarding recursive needs of tactic glob/interp/eval functions *) - -let _ = - (** FIXME: use generic internalization *) - let f l tac = - let tac = out_gen (rawwit Constrarg.wit_ltac) tac in - let ltacvars = - List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l - in - Flags.with_option strict_check - (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars }) tac - in - Hook.set Hints.extern_intern_tac f |