diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 6f0d7525d..6d50c02e2 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 *) |