diff options
| -rw-r--r-- | tactics/auto.ml | 10 | ||||
| -rw-r--r-- | tactics/auto.mli | 5 | ||||
| -rw-r--r-- | tactics/hints.ml | 7 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 |
5 files changed, 13 insertions, 17 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 761c41da6..fc6ff03b4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -140,8 +140,6 @@ si après Intros la conclusion matche le pattern. (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *) -let (forward_interp_tactic, extern_interp) = Hook.make () - let conclPattern concl pat tac = let constr_bindings env sigma = match pat with @@ -156,7 +154,13 @@ let conclPattern concl pat tac = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in constr_bindings env sigma >>= fun constr_bindings -> - Hook.get forward_interp_tactic constr_bindings tac + let open Genarg in + let open Geninterp in + let inj c = Val.Dyn (val_tag (topwit Constrarg.wit_constr), c) in + let fold id c accu = Id.Map.add id (inj c) accu in + let lfun = Id.Map.fold fold constr_bindings Id.Map.empty in + let ist = { lfun; extra = TacStore.empty } in + Ftactic.run (Geninterp.generic_interp ist tac) (fun _ -> Proofview.tclUNIT ()) end } (***********************************************************) diff --git a/tactics/auto.mli b/tactics/auto.mli index cd2de99be..8c4f35904 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -13,9 +13,6 @@ open Pattern open Decl_kinds open Hints -val extern_interp : - (patvar_map -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic) Hook.t - (** Auto and related automation tactics *) val priority : ('a * full_hint) list -> ('a * full_hint) list @@ -35,7 +32,7 @@ val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clause [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the right values to build a tactic *) -val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic +val conclPattern : constr -> constr_pattern option -> Genarg.glob_generic_argument -> unit Proofview.tactic (** The Auto tactic *) diff --git a/tactics/hints.ml b/tactics/hints.ml index e5abad686..b2104ba43 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -76,7 +76,7 @@ type 'a hint_ast = | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) | Unfold_nth of evaluable_global_reference (* Hint Unfold *) - | Extern of glob_tactic_expr (* Hint Extern *) + | Extern of Genarg.glob_generic_argument (* Hint Extern *) type hints_path_atom = | PathHints of global_reference list @@ -749,6 +749,7 @@ 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; @@ -900,7 +901,7 @@ let subst_autohint (subst, obj) = let ref' = subst_evaluable_reference subst ref in if ref==ref' then data.code.obj else Unfold_nth ref' | Extern tac -> - let tac' = Tacsubst.subst_tactic subst tac in + let tac' = Genintern.generic_substitute subst tac in if tac==tac' then data.code.obj else Extern tac' in let name' = subst_path_atom subst data.name in @@ -1219,7 +1220,7 @@ let pr_hint h = match h.obj with env with e when Errors.noncritical e -> Global.env () in - (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac) + (str "(*external*) " ++ Pptactic.pr_glb_generic env tac) let pr_id_hint (id, v) = (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) diff --git a/tactics/hints.mli b/tactics/hints.mli index 3e08060f8..df9d79212 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -33,7 +33,7 @@ type 'a hint_ast = | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) | Unfold_nth of evaluable_global_reference (* Hint Unfold *) - | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) + | Extern of Genarg.glob_generic_argument (* Hint Extern *) type hint type raw_hint = constr * types * Univ.universe_context_set diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8afc73526..4506f8159 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2179,12 +2179,6 @@ let _ = in Hook.set Pretyping.genarg_interp_hook eval -let _ = Hook.set Auto.extern_interp - (fun l -> - let lfun = Id.Map.map (fun c -> Value.of_constr c) l in - let ist = { (default_ist ()) with lfun; } in - interp_tactic ist) - (** Used in tactic extension **) let dummy_id = Id.of_string "_" |