Removing the various glob/subst/interp registering functions for

extra argument types and putting them into Genarg.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16586 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 19 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index dc84fa592..5abba699e 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 *)