diff options
| -rw-r--r-- | grammar/argextend.ml4 | 13 | ||||
| -rw-r--r-- | parsing/extrawit.ml | 8 | ||||
| -rw-r--r-- | parsing/extrawit.mli | 2 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 14 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 18 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 13 |
6 files changed, 32 insertions, 36 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index eb4630394..dfcaa4e84 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -22,14 +22,11 @@ let qualified_name loc s = qualified_name loc path name let mk_extraarg loc s = - if Extrawit.tactic_genarg_level s = None then - try - let name = Genarg.get_name0 s in - qualified_name loc name - with Not_found -> - <:expr< $lid:"wit_"^s$ >> - else - qualified_name loc ("Extrawit.wit_" ^ s) + try + let name = Genarg.get_name0 s in + qualified_name loc name + with Not_found -> + <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >> diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index 8332bd49f..c20f43bd5 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -37,6 +37,8 @@ let tactic_genarg_level s = else None else None -let is_tactic_genarg = function -| ExtraArgType s -> tactic_genarg_level s <> None -| _ -> false +let () = + for i = 0 to 5 do + let name = Printf.sprintf "Extrawit.wit_tactic%i" i in + Genarg.register_name0 (wit_tactic i) name + done diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli index a74c8a259..1bd5cdb89 100644 --- a/parsing/extrawit.mli +++ b/parsing/extrawit.mli @@ -24,6 +24,4 @@ val wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_t val wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type val wit_tactic5 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type -val is_tactic_genarg : argument_type -> bool - val tactic_genarg_level : string -> int option 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 *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 58c64a831..67fa0ed7b 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 2e84d4425..006885616 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 |