diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 14 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 18 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 13 |
3 files changed, 22 insertions, 23 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 6f0d7525d1..6d50c02e24 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -795,13 +795,7 @@ and intern_genarg ist x = | OptArgType _ -> app_opt (intern_genarg ist) x | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x | ExtraArgType s -> - match tactic_genarg_level s with - | Some n -> - (* Special treatment of tactic arguments *) - in_gen (glbwit (wit_tactic n)) (intern_tactic_or_tacarg ist - (out_gen (rawwit (wit_tactic n)) x)) - | None -> - snd (Genintern.generic_intern ist x) + snd (Genintern.generic_intern ist x) (** Other entry points *) @@ -954,6 +948,12 @@ let () = in Genintern.register_intern0 wit_intro_pattern intern_intro_pattern +let () = + let intern ist tac = (ist, intern_tactic_or_tacarg ist tac) in + for i = 0 to 5 do + Genintern.register_intern0 (wit_tactic i) intern + done + (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 58c64a8317..67fa0ed7b2 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1451,15 +1451,6 @@ and interp_genarg ist gl x = | OptArgType _ -> app_opt (interp_genarg ist gl) x | PairArgType _ -> app_pair (interp_genarg ist gl) (interp_genarg ist gl) x | ExtraArgType s -> - match tactic_genarg_level s with - | Some n -> - let f = VFun(extract_trace ist,ist.lfun,[], - out_gen (glbwit (wit_tactic n)) x) - in - (* Special treatment of tactic arguments *) - in_gen (topwit (wit_tactic n)) - (TacArg(dloc,valueIn (of_tacvalue f))) - | None -> let (sigma,v) = Geninterp.generic_interp ist gl x in evdref:=sigma; v @@ -2068,6 +2059,15 @@ let () = let interp ist gl pat = (gl.sigma, interp_intro_pattern ist gl pat) in Geninterp.register_interp0 wit_intro_pattern interp +let () = + let interp ist gl tac = + let f = VFun (extract_trace ist, ist.lfun, [], tac) in + (gl.sigma, TacArg (dloc, valueIn (of_tacvalue f))) + in + for i = 0 to 5 do + Geninterp.register_interp0 (wit_tactic i) interp + done + (***************************************************************************) (* Other entry points *) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 2e84d44258..0068856162 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -322,16 +322,15 @@ and subst_genarg subst (x:glob_generic_argument) = | OptArgType _ -> app_opt (subst_genarg subst) x | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x | ExtraArgType s -> - match Extrawit.tactic_genarg_level s with - | Some n -> - (* Special treatment of tactic arguments *) - in_gen (glbwit (Extrawit.wit_tactic n)) - (subst_tactic subst (out_gen (glbwit (Extrawit.wit_tactic n)) x)) - | None -> - Genintern.generic_substitute subst x + Genintern.generic_substitute subst x (** Registering *) let () = Genintern.register_subst0 wit_intro_pattern (fun _ v -> v) +let () = + for i = 0 to 5 do + Genintern.register_subst0 (Extrawit.wit_tactic i) subst_tactic + done + let _ = Hook.set Auto.extern_subst_tactic subst_tactic |