diff options
| -rw-r--r-- | ltac/tacintern.ml | 20 | ||||
| -rw-r--r-- | tactics/hints.ml | 9 | ||||
| -rw-r--r-- | tactics/hints.mli | 7 |
3 files changed, 10 insertions, 26 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 diff --git a/tactics/hints.ml b/tactics/hints.ml index 9ee9e798b..a6d1fc6c8 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -804,7 +804,6 @@ let make_unfold eref = code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = - let tacast = Genarg.in_gen (Genarg.glbwit Constrarg.wit_ltac) tacast in let hdconstr = Option.map try_head_pattern pat in (hdconstr, { pri = pri; @@ -1082,8 +1081,6 @@ let add_trivials env sigma l local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let (forward_intern_tac, extern_intern_tac) = Hook.make () - type hnf = bool type hints_entry = @@ -1094,7 +1091,7 @@ type hints_entry = | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsModeEntry of global_reference * hint_mode list | HintsExternEntry of - int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr + int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument let default_prepare_hint_ident = Id.of_string "H" @@ -1184,7 +1181,9 @@ let interp_hints poly = | HintsExtern (pri, patcom, tacexp) -> let pat = Option.map fp patcom in let l = match pat with None -> [] | Some (l, _) -> l in - let tacexp = Hook.get forward_intern_tac l tacexp in + let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in + let env = Genintern.({ genv = env; ltacvars }) in + let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry (pri, pat, tacexp) let add_hints local dbnames0 h = diff --git a/tactics/hints.mli b/tactics/hints.mli index e38daca92..83876be84 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -134,7 +134,7 @@ type hints_entry = | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsModeEntry of global_reference * hint_mode list | HintsExternEntry of - int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr + int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument val searchtable_map : hint_db_name -> hint_db @@ -201,7 +201,7 @@ val make_resolve_hyp : (** [make_extern pri pattern tactic_expr] *) val make_extern : - int -> constr_pattern option -> Tacexpr.glob_tactic_expr + int -> constr_pattern option -> Genarg.glob_generic_argument -> hint_entry val run_hint : hint -> @@ -211,9 +211,6 @@ val run_hint : hint -> written code. *) val repr_hint : hint -> (raw_hint * clausenv) hint_ast -val extern_intern_tac : - (patvar list -> Genarg.raw_generic_argument -> Tacexpr.glob_tactic_expr) Hook.t - (** Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints; Boolean tells if lemmas with evars are allowed *) |