diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 20 | ||||
| -rw-r--r-- | tactics/tacintern.mli | 7 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 19 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 9 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 16 | ||||
| -rw-r--r-- | tactics/tacsubst.mli | 5 |
6 files changed, 7 insertions, 69 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index dc84fa5922..5abba699e3 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -67,24 +67,6 @@ let fully_empty_glob_sign = let make_empty_glob_sign () = { fully_empty_glob_sign with genv = Global.env () } -type intern_genarg_type = - glob_sign -> raw_generic_argument -> glob_generic_argument - -let genarginterns = - ref (String.Map.empty : intern_genarg_type String.Map.t) - -let add_intern_genarg id f = - genarginterns := String.Map.add id f !genarginterns - -let lookup_intern_genarg id = - try String.Map.find id !genarginterns - with Not_found -> - let msg = "No globalization function found for entry "^id in - Pp.msg_warning (Pp.strbrk msg); - let dflt = fun _ _ -> failwith msg in - add_intern_genarg id dflt; - dflt - (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Id.Map.empty @@ -821,7 +803,7 @@ and intern_genarg ist x = in_gen (glbwit (wit_tactic n)) (intern_tactic_or_tacarg ist (out_gen (rawwit (wit_tactic n)) x)) | None -> - lookup_intern_genarg s ist x + snd (Genarg.globalize ist x) (** Other entry points *) diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 75576516f4..ca33cf21ec 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -59,12 +59,7 @@ val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located (** Adds a globalization function for extra generic arguments *) -type intern_genarg_type = - glob_sign -> raw_generic_argument -> glob_generic_argument - -val add_intern_genarg : string -> intern_genarg_type -> unit - -val intern_genarg : intern_genarg_type +val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument (** Adds a definition of tactics in the table *) val add_tacdef : diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e52c2fe248..d9dc233b92 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -175,23 +175,6 @@ let () = (** Generic arguments : table of interpretation functions *) -type interp_genarg_type = - interp_sign -> goal sigma -> glob_generic_argument -> - Evd.evar_map * typed_generic_argument - -let extragenargtab = - ref (String.Map.empty : interp_genarg_type String.Map.t) -let add_interp_genarg id f = - extragenargtab := String.Map.add id f !extragenargtab -let lookup_interp_genarg id = - try String.Map.find id !extragenargtab - with Not_found -> - let msg = "No interpretation function found for entry " ^ id in - msg_warning (strbrk msg); - let f = fun _ _ _ -> failwith msg in - add_interp_genarg id f; - f - let push_trace (loc, ck) ist = match TacStore.get ist.extra f_trace with | None -> [1, loc, ck] | Some trace -> @@ -1458,7 +1441,7 @@ and interp_genarg ist gl x = in_gen (topwit (wit_tactic n)) (TacArg(dloc,valueIn (of_tacvalue f))) | None -> - let (sigma,v) = lookup_interp_genarg s ist gl x in + let (sigma,v) = interpret ist gl x in evdref:=sigma; v in diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index f079d1dfbd..254bb9fdd8 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -73,13 +73,8 @@ val get_debug : unit -> debug_info (** Adds an interpretation function for extra generic arguments *) -type interp_genarg_type = - interp_sign -> goal sigma -> glob_generic_argument -> - Evd.evar_map * typed_generic_argument - -val add_interp_genarg : string -> interp_genarg_type -> unit - -val interp_genarg : interp_genarg_type +val interp_genarg : interp_sign -> goal sigma -> glob_generic_argument -> + Evd.evar_map * typed_generic_argument (** Interprets any expression *) val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 3070cf01cc..f33e3ccec6 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -23,20 +23,6 @@ open Pretyping (** For generic arguments, we declare and store substitutions in a table *) -type subst_genarg_type = - substitution -> glob_generic_argument -> glob_generic_argument -let genargsubs = - ref (String.Map.empty : subst_genarg_type String.Map.t) -let add_genarg_subst id f = - genargsubs := String.Map.add id f !genargsubs -let lookup_genarg_subst id = - try String.Map.find id !genargsubs - with Not_found -> - Pp.msg_warning (Pp.strbrk ("No substitution found for entry "^id)); - let dflt = fun _ x -> x in - add_genarg_subst id dflt; - dflt - let subst_quantified_hypothesis _ x = x let subst_declared_or_quantified_hypothesis _ x = x @@ -346,6 +332,6 @@ and subst_genarg subst (x:glob_generic_argument) = in_gen (glbwit (Extrawit.wit_tactic n)) (subst_tactic subst (out_gen (glbwit (Extrawit.wit_tactic n)) x)) | None -> - lookup_genarg_subst s subst x + Genarg.substitute subst x let _ = Hook.set Auto.extern_subst_tactic subst_tactic diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli index ade3e7cc91..92640d4bc7 100644 --- a/tactics/tacsubst.mli +++ b/tactics/tacsubst.mli @@ -18,10 +18,7 @@ val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr (** For generic arguments, we declare and store substitutions in a table *) -type subst_genarg_type = - substitution -> glob_generic_argument -> glob_generic_argument -val subst_genarg : subst_genarg_type -val add_genarg_subst : string -> subst_genarg_type -> unit +val subst_genarg : substitution -> glob_generic_argument -> glob_generic_argument (** Misc *) |