Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp

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

25 files changed, 1549 insertions, 1372 deletions

diff --git a/dev/base_include b/dev/base_include
index 66d91f92e1..0f933d6684 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -140,6 +140,8 @@ open Hipattern
 open Inv
 open Leminv
 open Refine
+open Tacsubst
+open Tacintern
 open Tacinterp
 open Tacticals
 open Tactics
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index a3c94c5d4f..9c31e2c829 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -190,7 +190,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
     | None ->
 	<:expr< fun e x ->
           out_gen $make_globwit loc rawtyp$
-            (Tacinterp.intern_genarg e
+            (Tacintern.intern_genarg e
                (Genarg.in_gen $make_rawwit loc rawtyp$ x)) >>
     | Some f -> <:expr< $lid:f$>> in
   let interp = match f with
@@ -206,7 +206,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
     | None ->
 	<:expr< fun s x ->
           out_gen $make_globwit loc globtyp$
-	    (Tacinterp.subst_genarg s
+	    (Tacsubst.subst_genarg s
                (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
     | Some f -> <:expr< $lid:f$>> in
   let se = mlexpr_of_string s in
@@ -222,14 +222,16 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
      <:str_item<
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
      <:str_item< do {
+      Tacintern.add_intern_genarg $se$
+        (fun e x ->
+          (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x))));
       Tacinterp.add_interp_genarg $se$
-        ((fun e x ->
-          (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))),
         (fun ist gl x ->
 	  let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in
-          (sigma , Genarg.in_gen $wit$ a_interp)),
+          (sigma , Genarg.in_gen $wit$ a_interp));
+      Tacsubst.add_genarg_subst $se$
         (fun subst x ->
-          (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x)))));
+          (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))));
       Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
 	(None, [(None, None, $rules$)]);
       Pptactic.declare_extra_genarg_pprule
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 09c49b3b61..cebfaa6150 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -128,7 +128,7 @@ let rec possibly_empty_subentries loc = function
             <:expr< match Genarg.default_empty_value $rawwit$ with
                     [ None -> failwith ""
                     | Some v ->
-                        Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign
+                        Tacintern.intern_genarg Tacintern.fully_empty_glob_sign
                           (Genarg.in_gen $rawwit$ v) ] >>
         | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
             (* This does not parse epsilon (this Exit is static time) *)
@@ -159,11 +159,11 @@ let declare_tactic loc s cl =
   declare_str_items loc
     [ <:str_item< do {
       try
-        let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
+        let _=Tacintern.add_tactic $se$ $make_fun_clauses loc s cl$ in
         List.iter
           (fun (s,l) -> match l with
            [ Some l ->
-              Tacinterp.add_primitive_tactic s
+              Tacintern.add_primitive_tactic s
               (Tacexpr.TacAtom($default_loc$,
                  Tacexpr.TacExtend($default_loc$,$se$,l)))
            | None -> () ])
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 18232dce03..1f1388e3db 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -275,6 +275,7 @@ type glob_generic_argument = glevel generic_argument
 type typed_generic_argument = tlevel generic_argument
 
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
+type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen
 
 type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
diff --git a/parsing/g_obligations.ml4 b/parsing/g_obligations.ml4
index a0ea5c6dea..8d57bf2800 100644
--- a/parsing/g_obligations.ml4
+++ b/parsing/g_obligations.ml4
@@ -108,7 +108,7 @@ VERNAC COMMAND EXTEND Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
     set_default_tactic
       (Locality.use_section_locality ())
-      (Tacinterp.glob_tactic t) ]
+      (Tacintern.glob_tactic t) ]
 END
 
 open Pp
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index f2f978ccdf..5e185f7e39 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -10,6 +10,7 @@ open Errors
 open Util
 open Names
 open Constrexpr
+open Tacintern
 open Tacinterp
 open Decl_expr
 open Decl_mode
diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli
index bd6ed064e5..88fb9653ae 100644
--- a/plugins/decl_mode/decl_interp.mli
+++ b/plugins/decl_mode/decl_interp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Tacinterp
+open Tacintern
 open Decl_expr
 open Mod_subst
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 367e02bf8e..8075f05e9f 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -12,6 +12,7 @@ open Pp
 open Evd
 
 open Tacmach
+open Tacintern
 open Tacinterp
 open Decl_expr
 open Decl_mode
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index a3052320cf..c2b286f1b3 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -102,19 +102,20 @@ let proof_instr = Gram.entry_create "proofmode:instr"
 (* [Genarg.create_arg] creates a new embedding into Genarg. *)
 let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) =
   Genarg.create_arg None "proof_instr"
-let _ = Tacinterp.add_interp_genarg "proof_instr"
-  begin
+let _ = Tacintern.add_intern_genarg "proof_instr"
   begin fun e x -> (* declares the globalisation function *)
     Genarg.in_gen globwit_proof_instr 
       (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x))
-  end,
+  end
+let _ = Tacinterp.add_interp_genarg "proof_instr"
   begin fun ist gl x -> (* declares the interpretation function *)
     Tacmach.project gl ,
     Genarg.in_gen wit_proof_instr 
       (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x))
-  end,
-  begin fun _ x -> x end (* declares the substitution function, irrelevant in our case *)
-   end
+  end
+(* declares the substitution function, irrelevant in our case : *)
+let _ = Tacsubst.add_genarg_subst "proof_instr" (fun _ x -> x)
+
 
 let _ = Pptactic.declare_extra_genarg_pprule
   (rawwit_proof_instr, pr_raw_proof_instr)
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 160ca1b4c0..94fce0e47e 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -57,7 +57,7 @@ VERNAC COMMAND EXTEND Firstorder_Set_Solver
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
     set_default_solver 
       (Locality.use_section_locality ())
-      (Tacinterp.glob_tactic t) ]
+      (Tacintern.glob_tactic t) ]
 END
 
 VERNAC COMMAND EXTEND Firstorder_Print_Solver
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index f30ab7e8b4..fad762e9bd 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -186,7 +186,7 @@ let exec_tactic env n f args =
     TacId[] in
   let getter =
     Tacexp(TacFun(List.map(fun id -> Some id) lid,
-                  glob_tactic(tacticIn get_res))) in
+                  Tacintern.glob_tactic(tacticIn get_res))) in
   let _ =
     Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in
   !res
@@ -395,10 +395,10 @@ let subst_th (subst,th) =
   let th' = subst_mps subst th.ring_th in
   let thm1' = subst_mps subst th.ring_lemma1 in
   let thm2' = subst_mps subst th.ring_lemma2 in
-  let tac'= subst_tactic subst th.ring_cst_tac in
-  let pow_tac'= subst_tactic subst th.ring_pow_tac in
-  let pretac'= subst_tactic subst th.ring_pre_tac in
-  let posttac'= subst_tactic subst th.ring_post_tac in
+  let tac'= Tacsubst.subst_tactic subst th.ring_cst_tac in
+  let pow_tac'= Tacsubst.subst_tactic subst th.ring_pow_tac in
+  let pretac'= Tacsubst.subst_tactic subst th.ring_pre_tac in
+  let posttac'= Tacsubst.subst_tactic subst th.ring_post_tac in
   if c' == th.ring_carrier &&
      eq' == th.ring_req &&
      eq_constr set' th.ring_setoid &&
@@ -605,7 +605,7 @@ type cst_tac_spec =
 
 let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
   match cst_tac with
-      Some (CstTac t) -> Tacinterp.glob_tactic t
+      Some (CstTac t) -> Tacintern.glob_tactic t
     | Some (Closed lc) ->
         closed_term_ast (List.map Smartlocate.global_with_alias lc)
     | None ->
@@ -649,7 +649,7 @@ let interp_power env pow =
   | Some (tac, spec) ->
       let tac =
         match tac with
-        | CstTac t -> Tacinterp.glob_tactic t
+        | CstTac t -> Tacintern.glob_tactic t
         | Closed lc ->
             closed_term_ast (List.map Smartlocate.global_with_alias lc) in
       let spec = make_hyp env (ic spec) in
@@ -695,11 +695,11 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let posttac =
     match post with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let _ =
     Lib.add_leaf name
@@ -974,10 +974,10 @@ let subst_th (subst,th) =
   let thm3' = subst_mps subst th.field_simpl_ok in
   let thm4' = subst_mps subst th.field_simpl_eq_in_ok in
   let thm5' = subst_mps subst th.field_cond in
-  let tac'= subst_tactic subst th.field_cst_tac in
-  let pow_tac' = subst_tactic subst th.field_pow_tac in
-  let pretac'= subst_tactic subst th.field_pre_tac in
-  let posttac'= subst_tactic subst th.field_post_tac in
+  let tac'= Tacsubst.subst_tactic subst th.field_cst_tac in
+  let pow_tac' = Tacsubst.subst_tactic subst th.field_pow_tac in
+  let pretac'= Tacsubst.subst_tactic subst th.field_pre_tac in
+  let posttac'= Tacsubst.subst_tactic subst th.field_post_tac in
   if c' == th.field_carrier &&
      eq' == th.field_req &&
      thm1' == th.field_ok &&
@@ -1058,11 +1058,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
     match pre with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let posttac =
     match post with
-        Some t -> Tacinterp.glob_tactic t
+        Some t -> Tacintern.glob_tactic t
       | _ -> TacId [] in
   let _ =
     Lib.add_leaf name
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 686d2ae2de..2df8b8ce53 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -64,7 +64,7 @@ let sep_end = function
 (* Warning: [pr_raw_tactic] globalises and fails if globalisation fails *)
 
 let pr_raw_tactic_env l env t =
-  pr_glob_tactic env (Tacinterp.glob_tactic_env l env t)
+  pr_glob_tactic env (Tacintern.glob_tactic_env l env t)
 
 let pr_gen env t =
   pr_raw_generic
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index dd02475dd3..6a96d5bb7c 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -31,7 +31,7 @@ let subst_hint subst hint =
   let cst' = subst_mps subst hint.rew_lemma in
   let typ' = subst_mps subst hint.rew_type in
   let pat' = subst_mps subst hint.rew_pat in
-  let t' = Tacinterp.subst_tactic subst hint.rew_tac in
+  let t' = Tacsubst.subst_tactic subst hint.rew_tac in
     if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else
       { hint with
 	rew_lemma = cst'; rew_type = typ';
@@ -295,7 +295,7 @@ let add_rew_rules base lrul =
 	let pat = if b then info.hyp_left else info.hyp_right in
 	let rul = { rew_lemma = c; rew_type = info.hyp_ty;
 		    rew_pat = pat; rew_l2r = b;
-		    rew_tac = Tacinterp.glob_tactic t}
+		    rew_tac = Tacintern.glob_tactic t}
 	in incr counter;
 	  HintDN.add pat (!counter, rul) dn) HintDN.empty lrul
   in Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index e0ba730cdc..5c2746986d 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -99,9 +99,9 @@ let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob
 
 let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
 
-let glob_glob = Tacinterp.intern_constr
+let glob_glob = Tacintern.intern_constr
 
-let subst_glob = Tacinterp.subst_glob_constr_and_expr
+let subst_glob = Tacsubst.subst_glob_constr_and_expr
 
 ARGUMENT EXTEND glob
     PRINTED BY pr_globc
@@ -138,11 +138,11 @@ let pr_hloc = pr_loc_place () () ()
 
 let intern_place ist = function
     ConclLocation () -> ConclLocation ()
-  | HypLocation (id,hl) -> HypLocation (intern_hyp ist id,hl)
+  | HypLocation (id,hl) -> HypLocation (Tacintern.intern_hyp ist id,hl)
 
 let interp_place ist gl = function
     ConclLocation () -> ConclLocation ()
-  | HypLocation (id,hl) -> HypLocation (interp_hyp ist gl id,hl)
+  | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist gl id,hl)
 
 let interp_place ist gl p =
   Tacmach.project gl , interp_place ist gl p
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index f2075d07d5..bd6786a67f 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1379,8 +1379,9 @@ let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign
 let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) = Printer.pr_glob_constr (fst (fst ge))
 let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge)
 let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
-let glob_glob_constr_with_bindings ist l = Tacinterp.intern_constr_with_bindings ist l
-let subst_glob_constr_with_bindings s c = subst_glob_with_bindings s c
+let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
+let subst_glob_constr_with_bindings s c =
+  Tacsubst.subst_glob_with_bindings s c
 
 
 ARGUMENT EXTEND glob_constr_with_bindings 
@@ -1465,7 +1466,7 @@ type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast
 let interp_strategy ist gl s = 
   let sigma = project gl in
     sigma, strategy_of_ast s
-let glob_strategy ist s = map_strategy (Tacinterp.intern_constr ist) (fun c -> c) s
+let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s
 let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
new file mode 100644
index 0000000000..c601c623de
--- /dev/null
+++ b/tactics/tacintern.ml
@@ -0,0 +1,985 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Libobject
+open Pattern
+open Pp
+open Genredexpr
+open Glob_term
+open Tacred
+open Errors
+open Util
+open Names
+open Nameops
+open Libnames
+open Globnames
+open Nametab
+open Smartlocate
+open Constrexpr
+open Constrexpr_ops
+open Termops
+open Tacexpr
+open Genarg
+open Mod_subst
+open Extrawit
+open Misctypes
+open Locus
+
+(** Globalization of tactic expressions :
+    Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
+
+let dloc = Loc.ghost
+
+let error_global_not_found_loc (loc,qid) =
+  error_global_not_found_loc loc qid
+
+let error_syntactic_metavariables_not_allowed loc =
+  user_err_loc
+    (loc,"out_ident",
+     str "Syntactic metavariables allowed only in quotations.")
+
+let error_tactic_expected loc =
+  user_err_loc (loc,"",str "Tactic expected.")
+
+let skip_metaid = function
+  | AI x -> x
+  | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
+
+(** Generic arguments *)
+
+type glob_sign = {
+  ltacvars : identifier list * identifier list;
+     (* ltac variables and the subset of vars introduced by Intro/Let/... *)
+  ltacrecvars : (identifier * ltac_constant) list;
+     (* ltac recursive names *)
+  gsigma : Evd.evar_map;
+  genv : Environ.env }
+
+let fully_empty_glob_sign =
+  { ltacvars = ([],[]); ltacrecvars = [];
+    gsigma = Evd.empty; genv = Environ.empty_env }
+
+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 (Stringmap.empty : intern_genarg_type Stringmap.t)
+
+let add_intern_genarg id f =
+  genarginterns := Stringmap.add id f !genarginterns
+
+let lookup_intern_genarg id =
+  try Stringmap.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 Idmap.empty
+let add_primitive_tactic s tac =
+  let id = id_of_string s in
+  atomic_mactab := Idmap.add id tac !atomic_mactab
+
+let _ =
+  let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
+  List.iter
+      (fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t)))
+      [ "red", TacReduce(Red false,nocl);
+        "hnf", TacReduce(Hnf,nocl);
+        "simpl", TacReduce(Simpl None,nocl);
+        "compute", TacReduce(Cbv Redops.all_flags,nocl);
+        "intro", TacIntroMove(None,MoveLast);
+        "intros", TacIntroPattern [];
+        "assumption", TacAssumption;
+        "cofix", TacCofix None;
+        "trivial", TacTrivial (Off,[],None);
+        "auto", TacAuto(Off,None,[],None);
+        "left", TacLeft(false,NoBindings);
+        "eleft", TacLeft(true,NoBindings);
+        "right", TacRight(false,NoBindings);
+        "eright", TacRight(true,NoBindings);
+        "split", TacSplit(false,false,[NoBindings]);
+        "esplit", TacSplit(true,false,[NoBindings]);
+        "constructor", TacAnyConstructor (false,None);
+        "econstructor", TacAnyConstructor (true,None);
+        "reflexivity", TacReflexivity;
+        "symmetry", TacSymmetry nocl
+      ];
+  List.iter
+      (fun (s,t) -> add_primitive_tactic s t)
+      [ "idtac",TacId [];
+        "fail", TacFail(ArgArg 0,[]);
+        "fresh", TacArg(dloc,TacFreshId [])
+      ]
+
+let lookup_atomic id = Idmap.find id !atomic_mactab
+let is_atomic_kn kn =
+  let (_,_,l) = repr_kn kn in
+  Idmap.mem (id_of_label l) !atomic_mactab
+
+(* Tactics table (TacExtend). *)
+
+let tac_tab = Hashtbl.create 17
+
+let add_tactic s t =
+  if Hashtbl.mem tac_tab s then
+    errorlabstrm ("Refiner.add_tactic: ")
+      (str ("Cannot redeclare tactic "^s^"."));
+  Hashtbl.add tac_tab s t
+
+let overwriting_add_tactic s t =
+  if Hashtbl.mem tac_tab s then begin
+    Hashtbl.remove tac_tab s;
+    msg_warning (strbrk ("Overwriting definition of tactic "^s))
+  end;
+  Hashtbl.add tac_tab s t
+
+let lookup_tactic s =
+  try
+    Hashtbl.find tac_tab s
+  with Not_found ->
+    errorlabstrm "Refiner.lookup_tactic"
+      (str"The tactic " ++ str s ++ str" is not installed.")
+
+(* Summary and Object declaration *)
+
+let mactab = ref (Gmap.empty : (ltac_constant,glob_tactic_expr) Gmap.t)
+
+let lookup_ltacref r = Gmap.find r !mactab
+
+let _ =
+  Summary.declare_summary "tactic-definition"
+    { Summary.freeze_function   = (fun () -> !mactab);
+      Summary.unfreeze_function = (fun fs -> mactab := fs);
+      Summary.init_function     = (fun () -> mactab := Gmap.empty); }
+
+
+
+(* We have identifier <| global_reference <| constr *)
+
+let find_ident id ist =
+  List.mem id (fst ist.ltacvars) or
+  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
+
+let find_recvar qid ist = List.assoc qid ist.ltacrecvars
+
+(* a "var" is a ltac var or a var introduced by an intro tactic *)
+let find_var id ist = List.mem id (fst ist.ltacvars)
+
+(* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
+let find_ctxvar id ist = List.mem id (snd ist.ltacvars)
+
+(* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
+let find_ltacvar id ist = find_var id ist & not (find_ctxvar id ist)
+
+let find_hyp id ist =
+  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
+
+(* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
+(* be fresh in which case it is binding later on *)
+let intern_ident l ist id =
+  (* We use identifier both for variables and new names; thus nothing to do *)
+  if not (find_ident id ist) then l:=(id::fst !l,id::snd !l);
+  id
+
+let intern_name l ist = function
+  | Anonymous -> Anonymous
+  | Name id -> Name (intern_ident l ist id)
+
+let strict_check = ref false
+
+let adjust_loc loc = if !strict_check then dloc else loc
+
+(* Globalize a name which must be bound -- actually just check it is bound *)
+let intern_hyp ist (loc,id as locid) =
+  if not !strict_check then
+    locid
+  else if find_ident id ist then
+    (dloc,id)
+  else
+    Pretype_errors.error_var_not_found_loc loc id
+
+let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id)
+
+let intern_or_var ist = function
+  | ArgVar locid -> ArgVar (intern_hyp ist locid)
+  | ArgArg _ as x -> x
+
+let intern_inductive_or_by_notation = smart_global_inductive
+
+let intern_inductive ist = function
+  | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id)
+  | r -> ArgArg (intern_inductive_or_by_notation r)
+
+let intern_global_reference ist = function
+  | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
+  | r ->
+      let loc,_ as lqid = qualid_of_reference r in
+      try ArgArg (loc,locate_global_with_alias lqid)
+      with Not_found -> error_global_not_found_loc lqid
+
+let intern_ltac_variable ist = function
+  | Ident (loc,id) ->
+      if find_ltacvar id ist then
+	(* A local variable of any type *)
+	ArgVar (loc,id)
+      else
+      (* A recursive variable *)
+      ArgArg (loc,find_recvar id ist)
+  | _ ->
+      raise Not_found
+
+let intern_constr_reference strict ist = function
+  | Ident (_,id) as r when not strict & find_hyp id ist ->
+      GVar (dloc,id), Some (CRef r)
+  | Ident (_,id) as r when find_ctxvar id ist ->
+      GVar (dloc,id), if strict then None else Some (CRef r)
+  | r ->
+      let loc,_ as lqid = qualid_of_reference r in
+      GRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
+
+let intern_move_location ist = function
+  | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id)
+  | MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id)
+  | MoveFirst -> MoveFirst
+  | MoveLast -> MoveLast
+
+(* Internalize an isolated reference in position of tactic *)
+
+let intern_isolated_global_tactic_reference r =
+  let (loc,qid) = qualid_of_reference r in
+  try TacCall (loc,ArgArg (loc,locate_tactic qid),[])
+  with Not_found ->
+  match r with
+  | Ident (_,id) -> Tacexp (lookup_atomic id)
+  | _ -> raise Not_found
+
+let intern_isolated_tactic_reference strict ist r =
+  (* An ltac reference *)
+  try Reference (intern_ltac_variable ist r)
+  with Not_found ->
+  (* A global tactic *)
+  try intern_isolated_global_tactic_reference r
+  with Not_found ->
+  (* Tolerance for compatibility, allow not to use "constr:" *)
+  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+  with Not_found ->
+  (* Reference not found *)
+  error_global_not_found_loc (qualid_of_reference r)
+
+(* Internalize an applied tactic reference *)
+
+let intern_applied_global_tactic_reference r =
+  let (loc,qid) = qualid_of_reference r in
+  ArgArg (loc,locate_tactic qid)
+
+let intern_applied_tactic_reference ist r =
+  (* An ltac reference *)
+  try intern_ltac_variable ist r
+  with Not_found ->
+  (* A global tactic *)
+  try intern_applied_global_tactic_reference r
+  with Not_found ->
+  (* Reference not found *)
+  error_global_not_found_loc (qualid_of_reference r)
+
+(* Intern a reference parsed in a non-tactic entry *)
+
+let intern_non_tactic_reference strict ist r =
+  (* An ltac reference *)
+  try Reference (intern_ltac_variable ist r)
+  with Not_found ->
+  (* A constr reference *)
+  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+  with Not_found ->
+  (* Tolerance for compatibility, allow not to use "ltac:" *)
+  try intern_isolated_global_tactic_reference r
+  with Not_found ->
+  (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
+  match r with
+  | Ident (loc,id) when not strict -> IntroPattern (loc,IntroIdentifier id)
+  | _ ->
+  (* Reference not found *)
+  error_global_not_found_loc (qualid_of_reference r)
+
+let intern_message_token ist = function
+  | (MsgString _ | MsgInt _ as x) -> x
+  | MsgIdent id -> MsgIdent (intern_hyp_or_metaid ist id)
+
+let intern_message ist = List.map (intern_message_token ist)
+
+let rec intern_intro_pattern lf ist = function
+  | loc, IntroOrAndPattern l ->
+      loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
+  | loc, IntroIdentifier id ->
+      loc, IntroIdentifier (intern_ident lf ist id)
+  | loc, IntroFresh id ->
+      loc, IntroFresh (intern_ident lf ist id)
+  | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _)
+      as x -> x
+
+and intern_or_and_intro_pattern lf ist =
+  List.map (List.map (intern_intro_pattern lf ist))
+
+let intern_quantified_hypothesis ist = function
+  | AnonHyp n -> AnonHyp n
+  | NamedHyp id ->
+      (* Uncomment to disallow "intros until n" in ltac when n is not bound *)
+      NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*))
+
+let intern_binding_name ist x =
+  (* We use identifier both for variables and binding names *)
+  (* Todo: consider the body of the lemma to which the binding refer
+     and if a term w/o ltac vars, check the name is indeed quantified *)
+  x
+
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
+  let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
+  let c' =
+    warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
+  in
+  (c',if !strict_check then None else Some c)
+
+let intern_constr = intern_constr_gen false false
+let intern_type = intern_constr_gen false true
+
+(* Globalize bindings *)
+let intern_binding ist (loc,b,c) =
+  (loc,intern_binding_name ist b,intern_constr ist c)
+
+let intern_bindings ist = function
+  | NoBindings -> NoBindings
+  | ImplicitBindings l -> ImplicitBindings (List.map (intern_constr ist) l)
+  | ExplicitBindings l -> ExplicitBindings (List.map (intern_binding ist) l)
+
+let intern_constr_with_bindings ist (c,bl) =
+  (intern_constr ist c, intern_bindings ist bl)
+
+  (* TODO: catch ltac vars *)
+let intern_induction_arg ist = function
+  | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c)
+  | ElimOnAnonHyp n as x -> x
+  | ElimOnIdent (loc,id) ->
+      if !strict_check then
+	(* If in a defined tactic, no intros-until *)
+	match intern_constr ist (CRef (Ident (dloc,id))) with
+	| GVar (loc,id),_ -> ElimOnIdent (loc,id)
+	| c -> ElimOnConstr (c,NoBindings)
+      else
+	ElimOnIdent (loc,id)
+
+let short_name = function
+  | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
+  | _ -> None
+
+let intern_evaluable_global_reference ist r =
+  let lqid = qualid_of_reference r in
+  try evaluable_of_global_reference ist.genv (locate_global_with_alias lqid)
+  with Not_found ->
+  match r with
+  | Ident (loc,id) when not !strict_check -> EvalVarRef id
+  | _ -> error_global_not_found_loc lqid
+
+let intern_evaluable_reference_or_by_notation ist = function
+  | AN r -> intern_evaluable_global_reference ist r
+  | ByNotation (loc,ntn,sc) ->
+      evaluable_of_global_reference ist.genv
+      (Notation.interp_notation_as_global_reference loc
+        (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+
+(* Globalize a reduction expression *)
+let intern_evaluable ist = function
+  | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
+  | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist ->
+      ArgArg (EvalVarRef id, Some (loc,id))
+  | AN (Ident (loc,id)) when find_ctxvar id ist ->
+      ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id))
+  | r ->
+      let e = intern_evaluable_reference_or_by_notation ist r in
+      let na = short_name r in
+      ArgArg (e,na)
+
+let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
+
+let intern_flag ist red =
+  { red with rConst = List.map (intern_evaluable ist) red.rConst }
+
+let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
+
+let intern_constr_pattern ist ltacvars pc =
+  let metas,pat =
+    Constrintern.intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
+  let c = intern_constr_gen true false ist pc in
+  metas,(c,pat)
+
+let intern_typed_pattern ist p =
+  let dummy_pat = PRel 0 in
+  (* we cannot ensure in non strict mode that the pattern is closed *)
+  (* keeping a constr_expr copy is too complicated and we want anyway to *)
+  (* type it, so we remember the pattern as a glob_constr only *)
+  (intern_constr_gen true false ist p,dummy_pat)
+
+let intern_typed_pattern_with_occurrences ist (l,p) =
+  (l,intern_typed_pattern ist p)
+
+(* This seems fairly hacky, but it's the first way I've found to get proper
+   globalization of [unfold].  --adamc *)
+let dump_glob_red_expr = function
+  | Unfold occs -> List.iter (fun (_, r) ->
+    try
+      Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
+	(Smartlocate.smart_global r)
+    with _ -> ()) occs
+  | Cbv grf | Lazy grf ->
+    List.iter (fun r ->
+      try
+        Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
+	  (Smartlocate.smart_global r)
+      with _ -> ()) grf.rConst
+  | _ -> ()
+
+let intern_red_expr ist = function
+  | Unfold l -> Unfold (List.map (intern_unfold ist) l)
+  | Fold l -> Fold (List.map (intern_constr ist) l)
+  | Cbv f -> Cbv (intern_flag ist f)
+  | Lazy f -> Lazy (intern_flag ist f)
+  | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
+  | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o)
+  | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_with_occurrences ist) o)
+  | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
+
+let intern_in_hyp_as ist lf (id,ipat) =
+  (intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat)
+
+let intern_hyp_list ist = List.map (intern_hyp_or_metaid ist)
+
+let intern_inversion_strength lf ist = function
+  | NonDepInversion (k,idl,ids) ->
+      NonDepInversion (k,intern_hyp_list ist idl,
+      Option.map (intern_intro_pattern lf ist) ids)
+  | DepInversion (k,copt,ids) ->
+      DepInversion (k, Option.map (intern_constr ist) copt,
+      Option.map (intern_intro_pattern lf ist) ids)
+  | InversionUsing (c,idl) ->
+      InversionUsing (intern_constr ist c, intern_hyp_list ist idl)
+
+(* Interprets an hypothesis name *)
+let intern_hyp_location ist ((occs,id),hl) =
+  ((Locusops.occurrences_map (List.map (intern_or_var ist)) occs,
+   intern_hyp_or_metaid ist id), hl)
+
+(* Reads a pattern *)
+let intern_pattern ist ?(as_type=false) lfun = function
+  | Subterm (b,ido,pc) ->
+      let ltacvars = (lfun,[]) in
+      let (metas,pc) = intern_constr_pattern ist ltacvars pc in
+      ido, metas, Subterm (b,ido,pc)
+  | Term pc ->
+      let ltacvars = (lfun,[]) in
+      let (metas,pc) = intern_constr_pattern ist ltacvars pc in
+      None, metas, Term pc
+
+let intern_constr_may_eval ist = function
+  | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
+  | ConstrContext (locid,c) ->
+      ConstrContext (intern_hyp ist locid,intern_constr ist c)
+  | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
+  | ConstrTerm c -> ConstrTerm (intern_constr ist c)
+
+
+(* Reads the hypotheses of a "match goal" rule *)
+let rec intern_match_goal_hyps ist lfun = function
+  | (Hyp ((_,na) as locna,mp))::tl ->
+      let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
+      let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
+      let lfun' = name_cons na (Option.List.cons ido lfun) in
+      lfun', metas1@metas2, Hyp (locna,pat)::hyps
+  | (Def ((_,na) as locna,mv,mp))::tl ->
+      let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
+      let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
+      let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
+      let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
+      lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
+  | [] -> lfun, [], []
+
+(* Utilities *)
+let extract_let_names lrc =
+  List.fold_right
+    (fun ((loc,name),_) l ->
+      if List.mem name l then
+	user_err_loc
+	  (loc, "glob_tactic", str "This variable is bound several times.");
+      name::l)
+    lrc []
+
+let clause_app f = function
+    { onhyps=None; concl_occs=nl } ->
+      { onhyps=None; concl_occs=nl }
+  | { onhyps=Some l; concl_occs=nl } ->
+      { onhyps=Some(List.map f l); concl_occs=nl}
+
+(* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
+let rec intern_atomic lf ist x =
+  match (x:raw_atomic_tactic_expr) with
+  (* Basic tactics *)
+  | TacIntroPattern l ->
+      TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
+  | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
+  | TacIntroMove (ido,hto) ->
+      TacIntroMove (Option.map (intern_ident lf ist) ido,
+                    intern_move_location ist hto)
+  | TacAssumption -> TacAssumption
+  | TacExact c -> TacExact (intern_constr ist c)
+  | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
+  | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
+  | TacApply (a,ev,cb,inhyp) ->
+      TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
+                Option.map (intern_in_hyp_as ist lf) inhyp)
+  | TacElim (ev,cb,cbo) ->
+      TacElim (ev,intern_constr_with_bindings ist cb,
+               Option.map (intern_constr_with_bindings ist) cbo)
+  | TacElimType c -> TacElimType (intern_type ist c)
+  | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
+  | TacCaseType c -> TacCaseType (intern_type ist c)
+  | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
+  | TacMutualFix (id,n,l) ->
+      let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
+      TacMutualFix (intern_ident lf ist id, n, List.map f l)
+  | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
+  | TacMutualCofix (id,l) ->
+      let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
+      TacMutualCofix (intern_ident lf ist id, List.map f l)
+  | TacCut c -> TacCut (intern_type ist c)
+  | TacAssert (otac,ipat,c) ->
+      TacAssert (Option.map (intern_pure_tactic ist) otac,
+                 Option.map (intern_intro_pattern lf ist) ipat,
+                 intern_constr_gen false (otac<>None) ist c)
+  | TacGeneralize cl ->
+      TacGeneralize (List.map (fun (c,na) ->
+	               intern_constr_with_occurrences ist c,
+                       intern_name lf ist na) cl)
+  | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
+  | TacLetTac (na,c,cls,b,eqpat) ->
+      let na = intern_name lf ist na in
+      TacLetTac (na,intern_constr ist c,
+                 (clause_app (intern_hyp_location ist) cls),b,
+		 (Option.map (intern_intro_pattern lf ist) eqpat))
+
+  (* Automation tactics *)
+  | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
+  | TacAuto (d,n,lems,l) ->
+      TacAuto (d,Option.map (intern_or_var ist) n,
+        List.map (intern_constr ist) lems,l)
+
+  (* Derived basic tactics *)
+  | TacSimpleInductionDestruct (isrec,h) ->
+      TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
+  | TacInductionDestruct (ev,isrec,(l,el,cls)) ->
+      TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) ->
+	      (intern_induction_arg ist c,
+               (Option.map (intern_intro_pattern lf ist) ipato,
+	        Option.map (intern_intro_pattern lf ist) ipats))) l,
+               Option.map (intern_constr_with_bindings ist) el,
+               Option.map (clause_app (intern_hyp_location ist)) cls))
+  | TacDoubleInduction (h1,h2) ->
+      let h1 = intern_quantified_hypothesis ist h1 in
+      let h2 = intern_quantified_hypothesis ist h2 in
+      TacDoubleInduction (h1,h2)
+  | TacDecomposeAnd c -> TacDecomposeAnd (intern_constr ist c)
+  | TacDecomposeOr c -> TacDecomposeOr (intern_constr ist c)
+  | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
+      TacDecompose (l,intern_constr ist c)
+  | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
+  | TacLApply c -> TacLApply (intern_constr ist c)
+
+  (* Context management *)
+  | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l)
+  | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
+  | TacMove (dep,id1,id2) ->
+    TacMove (dep,intern_hyp_or_metaid ist id1,intern_move_location ist id2)
+  | TacRename l ->
+      TacRename (List.map (fun (id1,id2) ->
+			     intern_hyp_or_metaid ist id1,
+			     intern_hyp_or_metaid ist id2) l)
+  | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
+
+  (* Constructors *)
+  | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
+  | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
+  | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll)
+  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_pure_tactic ist) t)
+  | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl)
+
+  (* Conversion *)
+  | TacReduce (r,cl) ->
+      dump_glob_red_expr r;
+      TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
+  | TacChange (None,c,cl) ->
+      TacChange (None,
+        (if (cl.onhyps = None or cl.onhyps = Some []) &
+	    (cl.concl_occs = AllOccurrences or
+	     cl.concl_occs = NoOccurrences)
+         then intern_type ist c else intern_constr ist c),
+	clause_app (intern_hyp_location ist) cl)
+  | TacChange (Some p,c,cl) ->
+      TacChange (Some (intern_typed_pattern ist p),intern_constr ist c,
+	clause_app (intern_hyp_location ist) cl)
+
+  (* Equivalence relations *)
+  | TacReflexivity -> TacReflexivity
+  | TacSymmetry idopt ->
+      TacSymmetry (clause_app (intern_hyp_location ist) idopt)
+  | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c)
+
+  (* Equality and inversion *)
+  | TacRewrite (ev,l,cl,by) ->
+      TacRewrite
+	(ev,
+	List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
+	clause_app (intern_hyp_location ist) cl,
+	Option.map (intern_pure_tactic ist) by)
+  | TacInversion (inv,hyp) ->
+      TacInversion (intern_inversion_strength lf ist inv,
+        intern_quantified_hypothesis ist hyp)
+
+  (* For extensions *)
+  | TacExtend (loc,opn,l) ->
+      let _ = lookup_tactic opn in
+      TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
+  | TacAlias (loc,s,l,(dir,body)) ->
+      let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
+      TacAlias (loc,s,l,(dir,body))
+
+and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
+
+and intern_tactic_seq onlytac ist = function
+  | TacAtom (loc,t) ->
+      let lf = ref ist.ltacvars in
+      let t = intern_atomic lf ist t in
+      !lf, TacAtom (adjust_loc loc, t)
+  | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
+  | TacLetIn (isrec,l,u) ->
+      let (l1,l2) = ist.ltacvars in
+      let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in
+      let l = List.map (fun (n,b) ->
+	  (n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in
+      ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
+
+  | TacMatchGoal (lz,lr,lmr) ->
+      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr)
+  | TacMatch (lz,c,lmr) ->
+      ist.ltacvars,
+      TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
+  | TacId l -> ist.ltacvars, TacId (intern_message ist l)
+  | TacFail (n,l) ->
+      ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
+  | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)
+  | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac)
+  | TacAbstract (tac,s) ->
+      ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s)
+  | TacThen (t1,[||],t2,[||]) ->
+      let lfun', t1 = intern_tactic_seq onlytac ist t1 in
+      let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in
+      lfun'', TacThen (t1,[||],t2,[||])
+  | TacThen (t1,tf,t2,tl) ->
+      let lfun', t1 = intern_tactic_seq onlytac ist t1 in
+      let ist' = { ist with ltacvars = lfun' } in
+      (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
+      lfun', TacThen (t1,Array.map (intern_pure_tactic ist') tf,intern_pure_tactic ist' t2,
+		       Array.map (intern_pure_tactic ist') tl)
+  | TacThens (t,tl) ->
+      let lfun', t = intern_tactic_seq true ist t in
+      let ist' = { ist with ltacvars = lfun' } in
+      (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
+      lfun', TacThens (t, List.map (intern_pure_tactic ist') tl)
+  | TacDo (n,tac) ->
+      ist.ltacvars, TacDo (intern_or_var ist n,intern_pure_tactic ist tac)
+  | TacTry tac -> ist.ltacvars, TacTry (intern_pure_tactic ist tac)
+  | TacInfo tac -> ist.ltacvars, TacInfo (intern_pure_tactic ist tac)
+  | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac)
+  | TacTimeout (n,tac) ->
+      ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac)
+  | TacOrelse (tac1,tac2) ->
+      ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2)
+  | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l)
+  | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
+  | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
+  | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
+
+and intern_tactic_as_arg loc onlytac ist a =
+  match intern_tacarg !strict_check onlytac ist a with
+  | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ as a -> TacArg (loc,a)
+  | Tacexp a -> a
+  | TacVoid | IntroPattern _ | Integer _
+  | ConstrMayEval _ | TacFreshId _ as a ->
+      if onlytac then error_tactic_expected loc else TacArg (loc,a)
+  | MetaIdArg _ -> assert false
+
+and intern_tactic_or_tacarg ist = intern_tactic false ist
+
+and intern_pure_tactic ist = intern_tactic true ist
+
+and intern_tactic_fun ist (var,body) =
+  let (l1,l2) = ist.ltacvars in
+  let lfun' = List.rev_append (Option.List.flatten var) l1 in
+  (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body)
+
+and intern_tacarg strict onlytac ist = function
+  | TacVoid -> TacVoid
+  | Reference r -> intern_non_tactic_reference strict ist r
+  | IntroPattern ipat ->
+      let lf = ref([],[]) in (*How to know what names the intropattern binds?*)
+      IntroPattern (intern_intro_pattern lf ist ipat)
+  | Integer n -> Integer n
+  | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
+  | MetaIdArg (loc,istac,s) ->
+      (* $id can occur in Grammar tactic... *)
+      let id = id_of_string s in
+      if find_ltacvar id ist then
+	if istac then Reference (ArgVar (adjust_loc loc,id))
+	else ConstrMayEval (ConstrTerm (GVar (adjust_loc loc,id), None))
+      else error_syntactic_metavariables_not_allowed loc
+  | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f
+  | TacCall (loc,f,l) ->
+      TacCall (loc,
+        intern_applied_tactic_reference ist f,
+        List.map (intern_tacarg !strict_check false ist) l)
+  | TacExternal (loc,com,req,la) ->
+      TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la)
+  | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
+  | Tacexp t -> Tacexp (intern_tactic onlytac ist t)
+  | TacDynamic(loc,t) as x ->
+      (match Dyn.tag t with
+	| "tactic" | "value" -> x
+        | "constr" -> if onlytac then error_tactic_expected loc else x
+	| s -> anomaly_loc (loc, "",
+                 str "Unknown dynamic: <" ++ str s ++ str ">"))
+
+(* Reads the rules of a Match Context or a Match *)
+and intern_match_rule onlytac ist = function
+  | (All tc)::tl ->
+      All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
+  | (Pat (rl,mp,tc))::tl ->
+      let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
+      let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
+      let ido,metas2,pat = intern_pattern ist lfun mp in
+      let metas = List.uniquize (metas1@metas2) in
+      let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
+      Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
+  | [] -> []
+
+and intern_genarg ist x =
+  match genarg_tag x with
+  | BoolArgType -> in_gen globwit_bool (out_gen rawwit_bool x)
+  | IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
+  | IntOrVarArgType ->
+      in_gen globwit_int_or_var
+        (intern_or_var ist (out_gen rawwit_int_or_var x))
+  | StringArgType ->
+      in_gen globwit_string (out_gen rawwit_string x)
+  | PreIdentArgType ->
+      in_gen globwit_pre_ident (out_gen rawwit_pre_ident x)
+  | IntroPatternArgType ->
+      let lf = ref ([],[]) in
+      (* how to know which names are bound by the intropattern *)
+      in_gen globwit_intro_pattern
+        (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x))
+  | IdentArgType b ->
+      let lf = ref ([],[]) in
+      in_gen (globwit_ident_gen b)
+	(intern_ident lf ist (out_gen (rawwit_ident_gen b) x))
+  | VarArgType ->
+      in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x))
+  | RefArgType ->
+      in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
+  | SortArgType ->
+      in_gen globwit_sort (out_gen rawwit_sort x)
+  | ConstrArgType ->
+      in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x))
+  | ConstrMayEvalArgType ->
+      in_gen globwit_constr_may_eval
+        (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
+  | QuantHypArgType ->
+      in_gen globwit_quant_hyp
+        (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
+  | RedExprArgType ->
+      in_gen globwit_red_expr (intern_red_expr ist (out_gen rawwit_red_expr x))
+  | OpenConstrArgType b ->
+      in_gen (globwit_open_constr_gen b)
+        ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
+  | ConstrWithBindingsArgType ->
+      in_gen globwit_constr_with_bindings
+        (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
+  | BindingsArgType ->
+      in_gen globwit_bindings
+        (intern_bindings ist (out_gen rawwit_bindings x))
+  | List0ArgType _ -> app_list0 (intern_genarg ist) x
+  | List1ArgType _ -> app_list1 (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 (globwit_tactic n) (intern_tactic_or_tacarg ist
+	    (out_gen (rawwit_tactic n) x))
+      | None ->
+          lookup_intern_genarg s ist x
+
+(** Other entry points *)
+
+let glob_tactic x =
+  Flags.with_option strict_check
+    (intern_pure_tactic (make_empty_glob_sign ())) x
+
+let glob_tactic_env l env x =
+  Flags.with_option strict_check
+  (intern_pure_tactic
+    { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
+    x
+
+(***************************************************************************)
+(* Tactic registration *)
+
+(* Declaration of the TAC-DEFINITION object *)
+let add (kn,td) = mactab := Gmap.add kn td !mactab
+let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
+
+type tacdef_kind =
+  | NewTac of identifier
+  | UpdateTac of ltac_constant
+
+let load_md i ((sp,kn),(local,defs)) =
+  let dp,_ = repr_path sp in
+  let mp,dir,_ = repr_kn kn in
+  List.iter (fun (id,t) ->
+    match id with
+      | NewTac id ->
+	  let sp = Libnames.make_path dp id in
+	  let kn = Names.make_kn mp dir (label_of_id id) in
+	    Nametab.push_tactic (Until i) sp kn;
+	    add (kn,t)
+      | UpdateTac kn -> replace (kn,t)) defs
+
+let open_md i ((sp,kn),(local,defs)) =
+  let dp,_ = repr_path sp in
+  let mp,dir,_ = repr_kn kn in
+  List.iter (fun (id,t) ->
+    match id with
+	NewTac id ->
+	  let sp = Libnames.make_path dp id in
+	  let kn = Names.make_kn mp dir (label_of_id id) in
+	    Nametab.push_tactic (Exactly i) sp kn
+      | UpdateTac kn -> ()) defs
+
+let cache_md x = load_md 1 x
+
+let subst_kind subst id =
+  match id with
+    | NewTac _ -> id
+    | UpdateTac kn -> UpdateTac (subst_kn subst kn)
+
+let subst_md (subst,(local,defs)) =
+  (local,
+   List.map (fun (id,t) ->
+     (subst_kind subst id,Tacsubst.subst_tactic subst t)) defs)
+
+let classify_md (local,defs as o) =
+  if local then Dispose else Substitute o
+
+let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj =
+  declare_object {(default_object "TAC-DEFINITION") with
+     cache_function  = cache_md;
+     load_function   = load_md;
+     open_function   = open_md;
+     subst_function = subst_md;
+     classify_function = classify_md}
+
+let split_ltac_fun = function
+  | TacFun (l,t) -> (l,t)
+  | t -> ([],t)
+
+let pr_ltac_fun_arg = function
+  | None -> spc () ++ str "_"
+  | Some id -> spc () ++ pr_id id
+
+let print_ltac id =
+ try
+  let kn = Nametab.locate_tactic id in
+  let l,t = split_ltac_fun (lookup_ltacref kn) in
+  hv 2 (
+    hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
+           prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
+    ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t)
+ with
+  Not_found ->
+   errorlabstrm "print_ltac"
+    (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
+
+open Libnames
+
+(* Adds a definition for tactics in the table *)
+let make_absolute_name ident repl =
+  let loc = loc_of_reference ident in
+  try
+    let id, kn =
+      if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident))
+      else let id = coerce_reference_to_id ident in
+	     Some id, Lib.make_kn id
+    in
+      if Gmap.mem kn !mactab then
+	if repl then id, kn
+	else
+	  user_err_loc (loc,"Tacinterp.add_tacdef",
+		       str "There is already an Ltac named " ++ pr_reference ident ++ str".")
+      else if is_atomic_kn kn then
+	user_err_loc (loc,"Tacinterp.add_tacdef",
+		     str "Reserved Ltac name " ++ pr_reference ident ++ str".")
+      else id, kn
+  with Not_found ->
+    user_err_loc (loc,"Tacinterp.add_tacdef",
+		 str "There is no Ltac named " ++ pr_reference ident ++ str".")
+
+let add_tacdef local isrec tacl =
+  let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
+  let ist =
+    { (make_empty_glob_sign ()) with ltacrecvars =
+	if isrec then List.map_filter
+	  (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun
+	else []} in
+  let gtacl =
+    List.map2 (fun (_,b,def) (id, qid) ->
+      let k = if b then UpdateTac qid else NewTac (Option.get id) in
+      let t = Flags.with_option strict_check (intern_tactic_or_tacarg ist) def in
+	(k, t))
+      tacl rfun in
+  let id0 = fst (List.hd rfun) in
+  let _ = match id0 with
+    | Some id0 -> ignore(Lib.add_leaf id0 (inMD (local,gtacl)))
+    | _ -> Lib.add_anonymous_leaf (inMD (local,gtacl)) in
+  List.iter
+    (fun (id,b,_) ->
+      Flags.if_verbose msg_info (Libnames.pr_reference id ++
+				 (if b then str " is redefined"
+				   else str " is defined")))
+    tacl
+
+(***************************************************************************)
+(* Backwarding recursive needs of tactic glob/interp/eval functions *)
+
+let _ = Auto.set_extern_intern_tac
+  (fun l ->
+    Flags.with_option strict_check
+    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars=(l,[])}))
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
new file mode 100644
index 0000000000..69a708d235
--- /dev/null
+++ b/tactics/tacintern.mli
@@ -0,0 +1,91 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Names
+open Proof_type
+open Tacmach
+open Tactic_debug
+open Term
+open Tacexpr
+open Genarg
+open Constrexpr
+open Mod_subst
+open Redexpr
+open Misctypes
+open Nametab
+
+(** Globalization of tactic expressions :
+    Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
+
+type glob_sign = {
+  ltacvars : identifier list * identifier list;
+  ltacrecvars : (identifier * ltac_constant) list;
+  gsigma : Evd.evar_map;
+  genv : Environ.env }
+
+val fully_empty_glob_sign : glob_sign
+
+val make_empty_glob_sign : unit -> glob_sign
+ (** same as [fully_empty_glob_sign], but with [Global.env()] as
+     environment *)
+
+(** Main globalization functions *)
+
+val glob_tactic : raw_tactic_expr -> glob_tactic_expr
+
+val glob_tactic_env :
+  identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
+
+(** Low-level variants *)
+
+val intern_pure_tactic : glob_sign -> raw_tactic_expr -> glob_tactic_expr
+
+val intern_tactic_or_tacarg :
+  glob_sign -> raw_tactic_expr -> Tacexpr.glob_tactic_expr
+
+val intern_constr : glob_sign -> constr_expr -> glob_constr_and_expr
+
+val intern_constr_with_bindings :
+  glob_sign -> constr_expr * constr_expr bindings ->
+  glob_constr_and_expr * glob_constr_and_expr bindings
+
+val intern_hyp : glob_sign -> identifier Loc.located -> identifier 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
+
+(** Adds a definition of tactics in the table *)
+val add_tacdef :
+  Vernacexpr.locality_flag -> bool ->
+  (Libnames.reference * bool * raw_tactic_expr) list -> unit
+val add_primitive_tactic : string -> glob_tactic_expr -> unit
+
+(** Tactic extensions *)
+val add_tactic :
+  string -> (typed_generic_argument list -> tactic) -> unit
+val overwriting_add_tactic :
+  string -> (typed_generic_argument list -> tactic) -> unit
+val lookup_tactic :
+  string -> (typed_generic_argument list) -> tactic
+
+val lookup_ltacref : ltac_constant -> glob_tactic_expr
+
+(** printing *)
+val print_ltac : Libnames.qualid -> std_ppcmds
+
+(** Reduction expressions *)
+
+val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
+val dump_glob_red_expr : raw_red_expr -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0f378464a8..3de8395258 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Constrintern
-open Libobject
 open Pattern
 open Patternops
 open Matching
@@ -23,28 +22,25 @@ open Nameops
 open Libnames
 open Globnames
 open Nametab
-open Smartlocate
 open Pfedit
 open Proof_type
 open Refiner
 open Tacmach
 open Tactic_debug
 open Constrexpr
-open Constrexpr_ops
 open Term
 open Termops
 open Tacexpr
 open Hiddentac
 open Genarg
-open Mod_subst
 open Printer
-open Inductiveops
 open Pretyping
 open Extrawit
 open Evd
 open Misctypes
 open Miscops
 open Locus
+open Tacintern
 
 let safe_msgnl s =
   let _ =
@@ -53,20 +49,6 @@ let safe_msgnl s =
   in
   pp_flush () 
 
-let error_syntactic_metavariables_not_allowed loc =
-  user_err_loc
-    (loc,"out_ident",
-     str "Syntactic metavariables allowed only in quotations.")
-
-let error_tactic_expected loc =
-  user_err_loc (loc,"",str "Tactic expected.")
-
-let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid
-
-let skip_metaid = function
-  | AI x -> x
-  | MetaId (loc,_) -> error_syntactic_metavariables_not_allowed loc
-
 (* Values for interpretation *)
 type value =
   | VRTactic of (goal list sigma) (* For Match results *)
@@ -138,6 +120,7 @@ let constr_of_id env id =
   Term.mkVar (let _ = Environ.lookup_named id env in id)
 
 (* To embed tactics *)
+
 let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t),
      (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) =
   Dyn.create "tactic"
@@ -147,120 +130,25 @@ let ((value_in : value -> Dyn.t),
 
 let valueIn t = TacDynamic (Loc.ghost,value_in t)
 
-(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
-let atomic_mactab = ref Idmap.empty
-let add_primitive_tactic s tac =
-  let id = id_of_string s in
-  atomic_mactab := Idmap.add id tac !atomic_mactab
-
-let _ =
-  let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
-  List.iter
-      (fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t)))
-      [ "red", TacReduce(Red false,nocl);
-        "hnf", TacReduce(Hnf,nocl);
-        "simpl", TacReduce(Simpl None,nocl);
-        "compute", TacReduce(Cbv Redops.all_flags,nocl);
-        "intro", TacIntroMove(None,MoveLast);
-        "intros", TacIntroPattern [];
-        "assumption", TacAssumption;
-        "cofix", TacCofix None;
-        "trivial", TacTrivial (Off,[],None);
-        "auto", TacAuto(Off,None,[],None);
-        "left", TacLeft(false,NoBindings);
-        "eleft", TacLeft(true,NoBindings);
-        "right", TacRight(false,NoBindings);
-        "eright", TacRight(true,NoBindings);
-        "split", TacSplit(false,false,[NoBindings]);
-        "esplit", TacSplit(true,false,[NoBindings]);
-        "constructor", TacAnyConstructor (false,None);
-        "econstructor", TacAnyConstructor (true,None);
-        "reflexivity", TacReflexivity;
-        "symmetry", TacSymmetry nocl
-      ];
-  List.iter
-      (fun (s,t) -> add_primitive_tactic s t)
-      [ "idtac",TacId [];
-        "fail", TacFail(ArgArg 0,[]);
-        "fresh", TacArg(dloc,TacFreshId [])
-      ]
-
-let lookup_atomic id = Idmap.find id !atomic_mactab
-let is_atomic_kn kn =
-  let (_,_,l) = repr_kn kn in
-  Idmap.mem (id_of_label l) !atomic_mactab
-
-(* Summary and Object declaration *)
-let mactab = ref Gmap.empty
-
-let lookup r = Gmap.find r !mactab
-
-let _ =
-  let init () = mactab := Gmap.empty in
-  let freeze () = !mactab in
-  let unfreeze fs = mactab := fs in
-  Summary.declare_summary "tactic-definition"
-    { Summary.freeze_function   = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init }
-
-(* Tactics table (TacExtend). *)
-
-let tac_tab = Hashtbl.create 17
-
-let add_tactic s t =
-  if Hashtbl.mem tac_tab s then
-    errorlabstrm ("Refiner.add_tactic: ")
-      (str ("Cannot redeclare tactic "^s^"."));
-  Hashtbl.add tac_tab s t
-
-let overwriting_add_tactic s t =
-  if Hashtbl.mem tac_tab s then begin
-    Hashtbl.remove tac_tab s;
-    msg_warning (strbrk ("Overwriting definition of tactic "^s))
-  end;
-  Hashtbl.add tac_tab s t
-
-let lookup_tactic s =
-  try
-    Hashtbl.find tac_tab s
-  with Not_found ->
-    errorlabstrm "Refiner.lookup_tactic"
-      (str"The tactic " ++ str s ++ str" is not installed.")
-
-(* Interpretation of extra generic arguments *)
-type glob_sign = {
-  ltacvars : identifier list * identifier list;
-     (* ltac variables and the subset of vars introduced by Intro/Let/... *)
-  ltacrecvars : (identifier * ltac_constant) list;
-     (* ltac recursive names *)
-  gsigma : Evd.evar_map;
-  genv : Environ.env }
+(** Generic arguments : table of interpretation functions *)
 
 type interp_genarg_type =
-  (glob_sign -> raw_generic_argument -> glob_generic_argument) *
-  (interp_sign -> goal sigma -> glob_generic_argument ->
-    Evd.evar_map * typed_generic_argument) *
-  (substitution -> glob_generic_argument -> glob_generic_argument)
+  interp_sign -> goal sigma -> glob_generic_argument ->
+    Evd.evar_map * typed_generic_argument
 
 let extragenargtab =
-  ref (Gmap.empty : (string,interp_genarg_type) Gmap.t)
+  ref (Stringmap.empty : interp_genarg_type Stringmap.t)
 let add_interp_genarg id f =
-  extragenargtab := Gmap.add id f !extragenargtab
-let lookup_genarg id =
-  try Gmap.find id !extragenargtab
+  extragenargtab := Stringmap.add id f !extragenargtab
+let lookup_interp_genarg id =
+  try Stringmap.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), (fun _ _ _ -> failwith msg), (fun _ a -> a) in
+    let f = fun _ _ _ -> failwith msg in
     add_interp_genarg id f;
     f
 
-
-let lookup_genarg_glob   id = let (f,_,_) = lookup_genarg id in f
-let lookup_interp_genarg id = let (_,f,_) = lookup_genarg id in f
-let lookup_genarg_subst  id = let (_,_,f) = lookup_genarg id in f
-
 let push_trace (loc,ck) = function
   | (n,loc',ck')::trl when ck=ck' -> (n+1,loc,ck)::trl
   | trl -> (1,loc,ck)::trl
@@ -277,342 +165,6 @@ let coerce_to_tactic loc id = function
   | _ -> user_err_loc
   (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
 
-(*****************)
-(* Globalization *)
-(*****************)
-
-(* We have identifier <| global_reference <| constr *)
-
-let find_ident id ist =
-  List.mem id (fst ist.ltacvars) or
-  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
-
-let find_recvar qid ist = List.assoc qid ist.ltacrecvars
-
-(* a "var" is a ltac var or a var introduced by an intro tactic *)
-let find_var id ist = List.mem id (fst ist.ltacvars)
-
-(* a "ctxvar" is a var introduced by an intro tactic (Intro/LetTac/...) *)
-let find_ctxvar id ist = List.mem id (snd ist.ltacvars)
-
-(* a "ltacvar" is an ltac var (Let-In/Fun/...) *)
-let find_ltacvar id ist = find_var id ist & not (find_ctxvar id ist)
-
-let find_hyp id ist =
-  List.mem id (ids_of_named_context (Environ.named_context ist.genv))
-
-(* Globalize a name introduced by Intro/LetTac/... ; it is allowed to *)
-(* be fresh in which case it is binding later on *)
-let intern_ident l ist id =
-  (* We use identifier both for variables and new names; thus nothing to do *)
-  if not (find_ident id ist) then l:=(id::fst !l,id::snd !l);
-  id
-
-let intern_name l ist = function
-  | Anonymous -> Anonymous
-  | Name id -> Name (intern_ident l ist id)
-
-let strict_check = ref false
-
-let adjust_loc loc = if !strict_check then dloc else loc
-
-(* Globalize a name which must be bound -- actually just check it is bound *)
-let intern_hyp ist (loc,id as locid) =
-  if not !strict_check then
-    locid
-  else if find_ident id ist then
-    (dloc,id)
-  else
-    Pretype_errors.error_var_not_found_loc loc id
-
-let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id)
-
-let intern_or_var ist = function
-  | ArgVar locid -> ArgVar (intern_hyp ist locid)
-  | ArgArg _ as x -> x
-
-let intern_inductive_or_by_notation = smart_global_inductive
-
-let intern_inductive ist = function
-  | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id)
-  | r -> ArgArg (intern_inductive_or_by_notation r)
-
-let intern_global_reference ist = function
-  | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
-  | r ->
-      let loc,_ as lqid = qualid_of_reference r in
-      try ArgArg (loc,locate_global_with_alias lqid)
-      with Not_found ->
-	error_global_not_found_loc lqid
-
-let intern_ltac_variable ist = function
-  | Ident (loc,id) ->
-      if find_ltacvar id ist then
-	(* A local variable of any type *)
-	ArgVar (loc,id)
-      else
-      (* A recursive variable *)
-      ArgArg (loc,find_recvar id ist)
-  | _ ->
-      raise Not_found
-
-let intern_constr_reference strict ist = function
-  | Ident (_,id) as r when not strict & find_hyp id ist ->
-      GVar (dloc,id), Some (CRef r)
-  | Ident (_,id) as r when find_ctxvar id ist ->
-      GVar (dloc,id), if strict then None else Some (CRef r)
-  | r ->
-      let loc,_ as lqid = qualid_of_reference r in
-      GRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
-
-let intern_move_location ist = function
-  | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id)
-  | MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id)
-  | MoveFirst -> MoveFirst
-  | MoveLast -> MoveLast
-
-(* Internalize an isolated reference in position of tactic *)
-
-let intern_isolated_global_tactic_reference r =
-  let (loc,qid) = qualid_of_reference r in
-  try TacCall (loc,ArgArg (loc,locate_tactic qid),[])
-  with Not_found ->
-  match r with
-  | Ident (_,id) -> Tacexp (lookup_atomic id)
-  | _ -> raise Not_found
-
-let intern_isolated_tactic_reference strict ist r =
-  (* An ltac reference *)
-  try Reference (intern_ltac_variable ist r)
-  with Not_found ->
-  (* A global tactic *)
-  try intern_isolated_global_tactic_reference r
-  with Not_found ->
-  (* Tolerance for compatibility, allow not to use "constr:" *)
-  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
-  with Not_found ->
-  (* Reference not found *)
-  error_global_not_found_loc (qualid_of_reference r)
-
-(* Internalize an applied tactic reference *)
-
-let intern_applied_global_tactic_reference r =
-  let (loc,qid) = qualid_of_reference r in
-  ArgArg (loc,locate_tactic qid)
-
-let intern_applied_tactic_reference ist r =
-  (* An ltac reference *)
-  try intern_ltac_variable ist r
-  with Not_found ->
-  (* A global tactic *)
-  try intern_applied_global_tactic_reference r
-  with Not_found ->
-  (* Reference not found *)
-  error_global_not_found_loc (qualid_of_reference r)
-
-(* Intern a reference parsed in a non-tactic entry *)
-
-let intern_non_tactic_reference strict ist r =
-  (* An ltac reference *)
-  try Reference (intern_ltac_variable ist r)
-  with Not_found ->
-  (* A constr reference *)
-  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
-  with Not_found ->
-  (* Tolerance for compatibility, allow not to use "ltac:" *)
-  try intern_isolated_global_tactic_reference r
-  with Not_found ->
-  (* By convention, use IntroIdentifier for unbound ident, when not in a def *)
-  match r with
-  | Ident (loc,id) when not strict -> IntroPattern (loc,IntroIdentifier id)
-  | _ ->
-  (* Reference not found *)
-  error_global_not_found_loc (qualid_of_reference r)
-
-let intern_message_token ist = function
-  | (MsgString _ | MsgInt _ as x) -> x
-  | MsgIdent id -> MsgIdent (intern_hyp_or_metaid ist id)
-
-let intern_message ist = List.map (intern_message_token ist)
-
-let rec intern_intro_pattern lf ist = function
-  | loc, IntroOrAndPattern l ->
-      loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
-  | loc, IntroIdentifier id ->
-      loc, IntroIdentifier (intern_ident lf ist id)
-  | loc, IntroFresh id ->
-      loc, IntroFresh (intern_ident lf ist id)
-  | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _)
-      as x -> x
-
-and intern_or_and_intro_pattern lf ist =
-  List.map (List.map (intern_intro_pattern lf ist))
-
-let intern_quantified_hypothesis ist = function
-  | AnonHyp n -> AnonHyp n
-  | NamedHyp id ->
-      (* Uncomment to disallow "intros until n" in ltac when n is not bound *)
-      NamedHyp ((*snd (intern_hyp ist (dloc,*)id(* ))*))
-
-let intern_binding_name ist x =
-  (* We use identifier both for variables and binding names *)
-  (* Todo: consider the body of the lemma to which the binding refer
-     and if a term w/o ltac vars, check the name is indeed quantified *)
-  x
-
-let intern_constr_gen allow_patvar isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
-  let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in
-  let c' =
-    warn (Constrintern.intern_gen isarity ~allow_patvar ~ltacvars:(fst lfun,[]) sigma env) c
-  in
-  (c',if !strict_check then None else Some c)
-
-let intern_constr = intern_constr_gen false false
-let intern_type = intern_constr_gen false true
-
-(* Globalize bindings *)
-let intern_binding ist (loc,b,c) =
-  (loc,intern_binding_name ist b,intern_constr ist c)
-
-let intern_bindings ist = function
-  | NoBindings -> NoBindings
-  | ImplicitBindings l -> ImplicitBindings (List.map (intern_constr ist) l)
-  | ExplicitBindings l -> ExplicitBindings (List.map (intern_binding ist) l)
-
-let intern_constr_with_bindings ist (c,bl) =
-  (intern_constr ist c, intern_bindings ist bl)
-
-  (* TODO: catch ltac vars *)
-let intern_induction_arg ist = function
-  | ElimOnConstr c -> ElimOnConstr (intern_constr_with_bindings ist c)
-  | ElimOnAnonHyp n as x -> x
-  | ElimOnIdent (loc,id) ->
-      if !strict_check then
-	(* If in a defined tactic, no intros-until *)
-	match intern_constr ist (CRef (Ident (dloc,id))) with
-	| GVar (loc,id),_ -> ElimOnIdent (loc,id)
-	| c -> ElimOnConstr (c,NoBindings)
-      else
-	ElimOnIdent (loc,id)
-
-let short_name = function
-  | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id)
-  | _ -> None
-
-let intern_evaluable_global_reference ist r =
-  let lqid = qualid_of_reference r in
-  try evaluable_of_global_reference ist.genv (locate_global_with_alias lqid)
-  with Not_found ->
-  match r with
-  | Ident (loc,id) when not !strict_check -> EvalVarRef id
-  | _ -> error_global_not_found_loc lqid
-
-let intern_evaluable_reference_or_by_notation ist = function
-  | AN r -> intern_evaluable_global_reference ist r
-  | ByNotation (loc,ntn,sc) ->
-      evaluable_of_global_reference ist.genv
-      (Notation.interp_notation_as_global_reference loc
-        (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
-
-(* Globalize a reduction expression *)
-let intern_evaluable ist = function
-  | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
-  | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist ->
-      ArgArg (EvalVarRef id, Some (loc,id))
-  | AN (Ident (loc,id)) when find_ctxvar id ist ->
-      ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id))
-  | r ->
-      let e = intern_evaluable_reference_or_by_notation ist r in
-      let na = short_name r in
-      ArgArg (e,na)
-
-let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
-
-let intern_flag ist red =
-  { red with rConst = List.map (intern_evaluable ist) red.rConst }
-
-let intern_constr_with_occurrences ist (l,c) = (l,intern_constr ist c)
-
-let intern_constr_pattern ist ltacvars pc =
-  let metas,pat =
-    Constrintern.intern_constr_pattern ist.gsigma ist.genv ~ltacvars pc in
-  let c = intern_constr_gen true false ist pc in
-  metas,(c,pat)
-
-let intern_typed_pattern ist p =
-  let dummy_pat = PRel 0 in
-  (* we cannot ensure in non strict mode that the pattern is closed *)
-  (* keeping a constr_expr copy is too complicated and we want anyway to *)
-  (* type it, so we remember the pattern as a glob_constr only *)
-  (intern_constr_gen true false ist p,dummy_pat)
-
-let intern_typed_pattern_with_occurrences ist (l,p) =
-  (l,intern_typed_pattern ist p)
-
-(* This seems fairly hacky, but it's the first way I've found to get proper
-   globalization of [unfold].  --adamc *)
-let dump_glob_red_expr = function
-  | Unfold occs -> List.iter (fun (_, r) ->
-    try
-      Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
-	(Smartlocate.smart_global r)
-    with _ -> ()) occs
-  | Cbv grf | Lazy grf ->
-    List.iter (fun r ->
-      try
-        Dumpglob.add_glob (loc_of_or_by_notation Libnames.loc_of_reference r)
-	  (Smartlocate.smart_global r)
-      with _ -> ()) grf.rConst
-  | _ -> ()
-
-let intern_red_expr ist = function
-  | Unfold l -> Unfold (List.map (intern_unfold ist) l)
-  | Fold l -> Fold (List.map (intern_constr ist) l)
-  | Cbv f -> Cbv (intern_flag ist f)
-  | Lazy f -> Lazy (intern_flag ist f)
-  | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
-  | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o)
-  | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_with_occurrences ist) o)
-  | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
-
-let intern_in_hyp_as ist lf (id,ipat) =
-  (intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat)
-
-let intern_hyp_list ist = List.map (intern_hyp_or_metaid ist)
-
-let intern_inversion_strength lf ist = function
-  | NonDepInversion (k,idl,ids) ->
-      NonDepInversion (k,intern_hyp_list ist idl,
-      Option.map (intern_intro_pattern lf ist) ids)
-  | DepInversion (k,copt,ids) ->
-      DepInversion (k, Option.map (intern_constr ist) copt,
-      Option.map (intern_intro_pattern lf ist) ids)
-  | InversionUsing (c,idl) ->
-      InversionUsing (intern_constr ist c, intern_hyp_list ist idl)
-
-(* Interprets an hypothesis name *)
-let intern_hyp_location ist ((occs,id),hl) =
-  ((Locusops.occurrences_map (List.map (intern_or_var ist)) occs,
-   intern_hyp_or_metaid ist id), hl)
-
-(* Reads a pattern *)
-let intern_pattern ist ?(as_type=false) lfun = function
-  | Subterm (b,ido,pc) ->
-      let ltacvars = (lfun,[]) in
-      let (metas,pc) = intern_constr_pattern ist ltacvars pc in
-      ido, metas, Subterm (b,ido,pc)
-  | Term pc ->
-      let ltacvars = (lfun,[]) in
-      let (metas,pc) = intern_constr_pattern ist ltacvars pc in
-      None, metas, Term pc
-
-let intern_constr_may_eval ist = function
-  | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c)
-  | ConstrContext (locid,c) ->
-      ConstrContext (intern_hyp ist locid,intern_constr ist c)
-  | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c)
-  | ConstrTerm c -> ConstrTerm (intern_constr ist c)
-
 (* External tactics *)
 let print_xml_term = ref (fun _ -> failwith "print_xml_term unset")
 let declare_xml_printer f = print_xml_term := f
@@ -640,347 +192,6 @@ let extend_values_with_bindings (ln,lm) lfun =
      binding of the same name exists *)
   lmatch@lfun@lnames
 
-(* Reads the hypotheses of a "match goal" rule *)
-let rec intern_match_goal_hyps ist lfun = function
-  | (Hyp ((_,na) as locna,mp))::tl ->
-      let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
-      let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
-      let lfun' = name_cons na (Option.List.cons ido lfun) in
-      lfun', metas1@metas2, Hyp (locna,pat)::hyps
-  | (Def ((_,na) as locna,mv,mp))::tl ->
-      let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
-      let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
-      let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
-      let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
-      lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
-  | [] -> lfun, [], []
-
-(* Utilities *)
-let extract_let_names lrc =
-  List.fold_right
-    (fun ((loc,name),_) l ->
-      if List.mem name l then
-	user_err_loc
-	  (loc, "glob_tactic", str "This variable is bound several times.");
-      name::l)
-    lrc []
-
-let clause_app f = function
-    { onhyps=None; concl_occs=nl } ->
-      { onhyps=None; concl_occs=nl }
-  | { onhyps=Some l; concl_occs=nl } ->
-      { onhyps=Some(List.map f l); concl_occs=nl}
-
-(* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
-let rec intern_atomic lf ist x =
-  match (x:raw_atomic_tactic_expr) with
-  (* Basic tactics *)
-  | TacIntroPattern l ->
-      TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
-  | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
-  | TacIntroMove (ido,hto) ->
-      TacIntroMove (Option.map (intern_ident lf ist) ido,
-                    intern_move_location ist hto)
-  | TacAssumption -> TacAssumption
-  | TacExact c -> TacExact (intern_constr ist c)
-  | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
-  | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
-  | TacApply (a,ev,cb,inhyp) ->
-      TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
-                Option.map (intern_in_hyp_as ist lf) inhyp)
-  | TacElim (ev,cb,cbo) ->
-      TacElim (ev,intern_constr_with_bindings ist cb,
-               Option.map (intern_constr_with_bindings ist) cbo)
-  | TacElimType c -> TacElimType (intern_type ist c)
-  | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
-  | TacCaseType c -> TacCaseType (intern_type ist c)
-  | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
-  | TacMutualFix (id,n,l) ->
-      let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
-      TacMutualFix (intern_ident lf ist id, n, List.map f l)
-  | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
-  | TacMutualCofix (id,l) ->
-      let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
-      TacMutualCofix (intern_ident lf ist id, List.map f l)
-  | TacCut c -> TacCut (intern_type ist c)
-  | TacAssert (otac,ipat,c) ->
-      TacAssert (Option.map (intern_pure_tactic ist) otac,
-                 Option.map (intern_intro_pattern lf ist) ipat,
-                 intern_constr_gen false (otac<>None) ist c)
-  | TacGeneralize cl ->
-      TacGeneralize (List.map (fun (c,na) ->
-	               intern_constr_with_occurrences ist c,
-                       intern_name lf ist na) cl)
-  | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
-  | TacLetTac (na,c,cls,b,eqpat) ->
-      let na = intern_name lf ist na in
-      TacLetTac (na,intern_constr ist c,
-                 (clause_app (intern_hyp_location ist) cls),b,
-		 (Option.map (intern_intro_pattern lf ist) eqpat))
-
-  (* Automation tactics *)
-  | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
-  | TacAuto (d,n,lems,l) ->
-      TacAuto (d,Option.map (intern_or_var ist) n,
-        List.map (intern_constr ist) lems,l)
-
-  (* Derived basic tactics *)
-  | TacSimpleInductionDestruct (isrec,h) ->
-      TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h)
-  | TacInductionDestruct (ev,isrec,(l,el,cls)) ->
-      TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) ->
-	      (intern_induction_arg ist c,
-               (Option.map (intern_intro_pattern lf ist) ipato,
-	        Option.map (intern_intro_pattern lf ist) ipats))) l,
-               Option.map (intern_constr_with_bindings ist) el,
-               Option.map (clause_app (intern_hyp_location ist)) cls))
-  | TacDoubleInduction (h1,h2) ->
-      let h1 = intern_quantified_hypothesis ist h1 in
-      let h2 = intern_quantified_hypothesis ist h2 in
-      TacDoubleInduction (h1,h2)
-  | TacDecomposeAnd c -> TacDecomposeAnd (intern_constr ist c)
-  | TacDecomposeOr c -> TacDecomposeOr (intern_constr ist c)
-  | TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
-      TacDecompose (l,intern_constr ist c)
-  | TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
-  | TacLApply c -> TacLApply (intern_constr ist c)
-
-  (* Context management *)
-  | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l)
-  | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l)
-  | TacMove (dep,id1,id2) ->
-    TacMove (dep,intern_hyp_or_metaid ist id1,intern_move_location ist id2)
-  | TacRename l ->
-      TacRename (List.map (fun (id1,id2) ->
-			     intern_hyp_or_metaid ist id1,
-			     intern_hyp_or_metaid ist id2) l)
-  | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l)
-
-  (* Constructors *)
-  | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl)
-  | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl)
-  | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll)
-  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_pure_tactic ist) t)
-  | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl)
-
-  (* Conversion *)
-  | TacReduce (r,cl) ->
-      dump_glob_red_expr r;
-      TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
-  | TacChange (None,c,cl) ->
-      TacChange (None,
-        (if (cl.onhyps = None or cl.onhyps = Some []) &
-	    (cl.concl_occs = AllOccurrences or
-	     cl.concl_occs = NoOccurrences)
-         then intern_type ist c else intern_constr ist c),
-	clause_app (intern_hyp_location ist) cl)
-  | TacChange (Some p,c,cl) ->
-      TacChange (Some (intern_typed_pattern ist p),intern_constr ist c,
-	clause_app (intern_hyp_location ist) cl)
-
-  (* Equivalence relations *)
-  | TacReflexivity -> TacReflexivity
-  | TacSymmetry idopt ->
-      TacSymmetry (clause_app (intern_hyp_location ist) idopt)
-  | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c)
-
-  (* Equality and inversion *)
-  | TacRewrite (ev,l,cl,by) ->
-      TacRewrite
-	(ev,
-	List.map (fun (b,m,c) -> (b,m,intern_constr_with_bindings ist c)) l,
-	clause_app (intern_hyp_location ist) cl,
-	Option.map (intern_pure_tactic ist) by)
-  | TacInversion (inv,hyp) ->
-      TacInversion (intern_inversion_strength lf ist inv,
-        intern_quantified_hypothesis ist hyp)
-
-  (* For extensions *)
-  | TacExtend (loc,opn,l) ->
-      let _ = lookup_tactic opn in
-      TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
-  | TacAlias (loc,s,l,(dir,body)) ->
-      let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
-      TacAlias (loc,s,l,(dir,body))
-
-and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
-
-and intern_tactic_seq onlytac ist = function
-  | TacAtom (loc,t) ->
-      let lf = ref ist.ltacvars in
-      let t = intern_atomic lf ist t in
-      !lf, TacAtom (adjust_loc loc, t)
-  | TacFun tacfun -> ist.ltacvars, TacFun (intern_tactic_fun ist tacfun)
-  | TacLetIn (isrec,l,u) ->
-      let (l1,l2) = ist.ltacvars in
-      let ist' = { ist with ltacvars = (extract_let_names l @ l1, l2) } in
-      let l = List.map (fun (n,b) ->
-	  (n,intern_tacarg !strict_check false (if isrec then ist' else ist) b)) l in
-      ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
-
-  | TacMatchGoal (lz,lr,lmr) ->
-      ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr)
-  | TacMatch (lz,c,lmr) ->
-      ist.ltacvars,
-      TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
-  | TacId l -> ist.ltacvars, TacId (intern_message ist l)
-  | TacFail (n,l) ->
-      ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
-  | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)
-  | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac)
-  | TacAbstract (tac,s) ->
-      ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s)
-  | TacThen (t1,[||],t2,[||]) ->
-      let lfun', t1 = intern_tactic_seq onlytac ist t1 in
-      let lfun'', t2 = intern_tactic_seq onlytac { ist with ltacvars = lfun' } t2 in
-      lfun'', TacThen (t1,[||],t2,[||])
-  | TacThen (t1,tf,t2,tl) ->
-      let lfun', t1 = intern_tactic_seq onlytac ist t1 in
-      let ist' = { ist with ltacvars = lfun' } in
-      (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
-      lfun', TacThen (t1,Array.map (intern_pure_tactic ist') tf,intern_pure_tactic ist' t2,
-		       Array.map (intern_pure_tactic ist') tl)
-  | TacThens (t,tl) ->
-      let lfun', t = intern_tactic_seq true ist t in
-      let ist' = { ist with ltacvars = lfun' } in
-      (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
-      lfun', TacThens (t, List.map (intern_pure_tactic ist') tl)
-  | TacDo (n,tac) ->
-      ist.ltacvars, TacDo (intern_or_var ist n,intern_pure_tactic ist tac)
-  | TacTry tac -> ist.ltacvars, TacTry (intern_pure_tactic ist tac)
-  | TacInfo tac -> ist.ltacvars, TacInfo (intern_pure_tactic ist tac)
-  | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_pure_tactic ist tac)
-  | TacTimeout (n,tac) ->
-      ist.ltacvars, TacTimeout (intern_or_var ist n,intern_tactic onlytac ist tac)
-  | TacOrelse (tac1,tac2) ->
-      ist.ltacvars, TacOrelse (intern_pure_tactic ist tac1,intern_pure_tactic ist tac2)
-  | TacFirst l -> ist.ltacvars, TacFirst (List.map (intern_pure_tactic ist) l)
-  | TacSolve l -> ist.ltacvars, TacSolve (List.map (intern_pure_tactic ist) l)
-  | TacComplete tac -> ist.ltacvars, TacComplete (intern_pure_tactic ist tac)
-  | TacArg (loc,a) -> ist.ltacvars, intern_tactic_as_arg loc onlytac ist a
-
-and intern_tactic_as_arg loc onlytac ist a =
-  match intern_tacarg !strict_check onlytac ist a with
-  | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ as a -> TacArg (loc,a)
-  | Tacexp a -> a
-  | TacVoid | IntroPattern _ | Integer _
-  | ConstrMayEval _ | TacFreshId _ as a ->
-      if onlytac then error_tactic_expected loc else TacArg (loc,a)
-  | MetaIdArg _ -> assert false
-
-and intern_tactic_or_tacarg ist = intern_tactic false ist
-
-and intern_pure_tactic ist = intern_tactic true ist
-
-and intern_tactic_fun ist (var,body) =
-  let (l1,l2) = ist.ltacvars in
-  let lfun' = List.rev_append (Option.List.flatten var) l1 in
-  (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body)
-
-and intern_tacarg strict onlytac ist = function
-  | TacVoid -> TacVoid
-  | Reference r -> intern_non_tactic_reference strict ist r
-  | IntroPattern ipat ->
-      let lf = ref([],[]) in (*How to know what names the intropattern binds?*)
-      IntroPattern (intern_intro_pattern lf ist ipat)
-  | Integer n -> Integer n
-  | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
-  | MetaIdArg (loc,istac,s) ->
-      (* $id can occur in Grammar tactic... *)
-      let id = id_of_string s in
-      if find_ltacvar id ist then
-	if istac then Reference (ArgVar (adjust_loc loc,id))
-	else ConstrMayEval (ConstrTerm (GVar (adjust_loc loc,id), None))
-      else error_syntactic_metavariables_not_allowed loc
-  | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f
-  | TacCall (loc,f,l) ->
-      TacCall (loc,
-        intern_applied_tactic_reference ist f,
-        List.map (intern_tacarg !strict_check false ist) l)
-  | TacExternal (loc,com,req,la) ->
-      TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la)
-  | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
-  | Tacexp t -> Tacexp (intern_tactic onlytac ist t)
-  | TacDynamic(loc,t) as x ->
-      (match Dyn.tag t with
-	| "tactic" | "value" -> x
-        | "constr" -> if onlytac then error_tactic_expected loc else x
-	| s -> anomaly_loc (loc, "",
-                 str "Unknown dynamic: <" ++ str s ++ str ">"))
-
-(* Reads the rules of a Match Context or a Match *)
-and intern_match_rule onlytac ist = function
-  | (All tc)::tl ->
-      All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
-  | (Pat (rl,mp,tc))::tl ->
-      let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in
-      let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
-      let ido,metas2,pat = intern_pattern ist lfun mp in
-      let metas = List.uniquize (metas1@metas2) in
-      let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in
-      Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
-  | [] -> []
-
-and intern_genarg ist x =
-  match genarg_tag x with
-  | BoolArgType -> in_gen globwit_bool (out_gen rawwit_bool x)
-  | IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
-  | IntOrVarArgType ->
-      in_gen globwit_int_or_var
-        (intern_or_var ist (out_gen rawwit_int_or_var x))
-  | StringArgType ->
-      in_gen globwit_string (out_gen rawwit_string x)
-  | PreIdentArgType ->
-      in_gen globwit_pre_ident (out_gen rawwit_pre_ident x)
-  | IntroPatternArgType ->
-      let lf = ref ([],[]) in
-      (* how to know which names are bound by the intropattern *)
-      in_gen globwit_intro_pattern
-        (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x))
-  | IdentArgType b ->
-      let lf = ref ([],[]) in
-      in_gen (globwit_ident_gen b)
-	(intern_ident lf ist (out_gen (rawwit_ident_gen b) x))
-  | VarArgType ->
-      in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x))
-  | RefArgType ->
-      in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
-  | SortArgType ->
-      in_gen globwit_sort (out_gen rawwit_sort x)
-  | ConstrArgType ->
-      in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x))
-  | ConstrMayEvalArgType ->
-      in_gen globwit_constr_may_eval
-        (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
-  | QuantHypArgType ->
-      in_gen globwit_quant_hyp
-        (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
-  | RedExprArgType ->
-      in_gen globwit_red_expr (intern_red_expr ist (out_gen rawwit_red_expr x))
-  | OpenConstrArgType b ->
-      in_gen (globwit_open_constr_gen b)
-        ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
-  | ConstrWithBindingsArgType ->
-      in_gen globwit_constr_with_bindings
-        (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
-  | BindingsArgType ->
-      in_gen globwit_bindings
-        (intern_bindings ist (out_gen rawwit_bindings x))
-  | List0ArgType _ -> app_list0 (intern_genarg ist) x
-  | List1ArgType _ -> app_list1 (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 (globwit_tactic n) (intern_tactic_or_tacarg ist
-	    (out_gen (rawwit_tactic n) x))
-      | None ->
-          lookup_genarg_glob s ist x
-
-(************* End globalization ************)
-
 (***************************************************************************)
 (* Evaluation/interpretation *)
 
@@ -1181,7 +392,7 @@ let interp_evaluable ist env = function
        with Not_found ->
        match r with
        | EvalConstRef _ -> r
-       | _ -> error_global_not_found_loc (loc,qualid_of_ident id))
+       | _ -> error_global_not_found_loc loc (qualid_of_ident id))
   | ArgArg (r,None) -> r
   | ArgVar locid ->
       interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
@@ -1846,7 +1057,7 @@ and interp_ltac_reference loc' mustbetac ist gl = function
       let ist =
         { lfun=[]; debug=ist.debug; avoid_ids=ids;
           trace = push_trace loc_info ist.trace } in
-      val_interp ist gl (lookup r)
+      val_interp ist gl (lookup_ltacref r)
 
 and interp_tacarg ist gl arg =
   let evdref = ref (project gl) in
@@ -2692,26 +1903,21 @@ and interp_atomic ist gl tac =
     let gl = { gl with sigma = !evdref } in
     interp_tactic { ist with lfun=lfun; trace=trace } body gl
 
-let make_empty_glob_sign () =
-  { ltacvars = ([],[]); ltacrecvars = [];
-    gsigma = Evd.empty; genv = Global.env() }
-
-let fully_empty_glob_sign =
-  { ltacvars = ([],[]); ltacrecvars = [];
-    gsigma = Evd.empty; genv = Environ.empty_env }
-
 (* Initial call for interpretation *)
-let interp_tac_gen lfun avoid_ids debug t gl =
-  interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] }
-    (intern_tactic true {
-      ltacvars = (List.map fst lfun, []); ltacrecvars = [];
-      gsigma = project gl; genv = pf_env gl } t) gl
 
 let eval_tactic t gls =
   db_initialize ();
   interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] }
     t gls
 
+(* globalization + interpretation *)
+
+let interp_tac_gen lfun avoid_ids debug t gl =
+  interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] }
+    (intern_pure_tactic {
+      ltacvars = (List.map fst lfun, []); ltacrecvars = [];
+      gsigma = project gl; genv = pf_env gl } t) gl
+
 let interp t = interp_tac_gen [] [] (get_debug()) t
 
 let eval_ltac_constr gl t =
@@ -2723,457 +1929,19 @@ let eval_ltac_constr gl t =
 let hide_interp t ot gl =
   let ist = { ltacvars = ([],[]); ltacrecvars = [];
             gsigma = project gl; genv = pf_env gl } in
-  let te = intern_tactic true ist t in
+  let te = intern_pure_tactic ist t in
   let t = eval_tactic te in
   match ot with
   | None -> t gl
   | Some t' -> (tclTHEN t t') gl
 
-(***************************************************************************)
-(* Substitution at module closing time *)
-
-let subst_quantified_hypothesis _ x = x
-
-let subst_declared_or_quantified_hypothesis _ x = x
-
-let subst_glob_constr_and_expr subst (c,e) =
-  assert (e=None); (* e<>None only for toplevel tactics *)
-  (Detyping.subst_glob_constr subst c,None)
-
-let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
-
-let subst_binding subst (loc,b,c) =
-  (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c)
-
-let subst_bindings subst = function
-  | NoBindings -> NoBindings
-  | ImplicitBindings l -> ImplicitBindings (List.map (subst_glob_constr subst) l)
-  | ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l)
-
-let subst_glob_with_bindings subst (c,bl) =
-  (subst_glob_constr subst c, subst_bindings subst bl)
-
-let subst_induction_arg subst = function
-  | ElimOnConstr c -> ElimOnConstr (subst_glob_with_bindings subst c)
-  | ElimOnAnonHyp n as x -> x
-  | ElimOnIdent id as x -> x
-
-let subst_and_short_name f (c,n) =
-(*  assert (n=None); *)(* since tacdef are strictly globalized *)
-  (f c,None)
-
-let subst_or_var f =  function
-  | ArgVar _ as x -> x
-  | ArgArg x -> ArgArg (f x)
-
-let subst_located f (_loc,id) = (dloc,f id)
-
-let subst_reference subst =
-  subst_or_var (subst_located (subst_kn subst))
-
-(*CSC: subst_global_reference is used "only" for RefArgType, that propagates
-  to the syntactic non-terminals "global", used in commands such as
-  Print. It is also used for non-evaluable references. *)
-let subst_global_reference subst =
- let subst_global ref =
-  let ref',t' = subst_global subst ref in
-   if not (eq_constr (constr_of_global ref') t') then
-    msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
-          str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
-          pr_global ref') ;
-   ref'
- in
-  subst_or_var (subst_located subst_global)
-
-let subst_evaluable subst =
-  let subst_eval_ref = subst_evaluable_reference subst in
-    subst_or_var (subst_and_short_name subst_eval_ref)
-
-let subst_unfold subst (l,e) =
-  (l,subst_evaluable subst e)
-
-let subst_flag subst red =
-  { red with rConst = List.map (subst_evaluable subst) red.rConst }
-
-let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
-
-let subst_glob_constr_or_pattern subst (c,p) =
-  (subst_glob_constr subst c,subst_pattern subst p)
-
-let subst_pattern_with_occurrences subst (l,p) =
-  (l,subst_glob_constr_or_pattern subst p)
-
-let subst_redexp subst = function
-  | Unfold l -> Unfold (List.map (subst_unfold subst) l)
-  | Fold l -> Fold (List.map (subst_glob_constr subst) l)
-  | Cbv f -> Cbv (subst_flag subst f)
-  | Lazy f -> Lazy (subst_flag subst f)
-  | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
-  | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o)
-  | CbvVm o -> CbvVm (Option.map (subst_pattern_with_occurrences subst) o)
-  | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
-
-let subst_raw_may_eval subst = function
-  | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c)
-  | ConstrContext (locid,c) -> ConstrContext (locid,subst_glob_constr subst c)
-  | ConstrTypeOf c -> ConstrTypeOf (subst_glob_constr subst c)
-  | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c)
-
-let subst_match_pattern subst = function
-  | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc))
-  | Term pc -> Term (subst_glob_constr_or_pattern subst pc)
-
-let rec subst_match_goal_hyps subst = function
-  | Hyp (locs,mp) :: tl ->
-      Hyp (locs,subst_match_pattern subst mp)
-      :: subst_match_goal_hyps subst tl
-  | Def (locs,mv,mp) :: tl ->
-      Def (locs,subst_match_pattern subst mv, subst_match_pattern subst mp)
-      :: subst_match_goal_hyps subst tl
-  | [] -> []
-
-let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
-  (* Basic tactics *)
-  | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
-  | TacAssumption as x -> x
-  | TacExact c -> TacExact (subst_glob_constr subst c)
-  | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c)
-  | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c)
-  | TacApply (a,ev,cb,cl) ->
-      TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl)
-  | TacElim (ev,cb,cbo) ->
-      TacElim (ev,subst_glob_with_bindings subst cb,
-               Option.map (subst_glob_with_bindings subst) cbo)
-  | TacElimType c -> TacElimType (subst_glob_constr subst c)
-  | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb)
-  | TacCaseType c -> TacCaseType (subst_glob_constr subst c)
-  | TacFix (idopt,n) as x -> x
-  | TacMutualFix (id,n,l) ->
-      TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
-  | TacCofix idopt as x -> x
-  | TacMutualCofix (id,l) ->
-      TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
-  | TacCut c -> TacCut (subst_glob_constr subst c)
-  | TacAssert (b,na,c) ->
-      TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
-  | TacGeneralize cl ->
-      TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
-  | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c)
-  | TacLetTac (id,c,clp,b,eqpat) ->
-    TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat)
-
-  (* Automation tactics *)
-  | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
-  | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
-
-  (* Derived basic tactics *)
-  | TacSimpleInductionDestruct (isrec,h) as x -> x
-  | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
-      let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in
-      let el' = Option.map (subst_glob_with_bindings subst) el in
-      TacInductionDestruct (isrec,ev,(l',el',cls))
-  | TacDoubleInduction (h1,h2) as x -> x
-  | TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c)
-  | TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c)
-  | TacDecompose (l,c) ->
-      let l = List.map (subst_or_var (subst_inductive subst)) l in
-      TacDecompose (l,subst_glob_constr subst c)
-  | TacSpecialize (n,l) -> TacSpecialize (n,subst_glob_with_bindings subst l)
-  | TacLApply c -> TacLApply (subst_glob_constr subst c)
-
-  (* Context management *)
-  | TacClear _ as x -> x
-  | TacClearBody l as x -> x
-  | TacMove (dep,id1,id2) as x -> x
-  | TacRename l as x -> x
-  | TacRevert _ as x -> x
-
-  (* Constructors *)
-  | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl)
-  | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl)
-  | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (subst_bindings subst) bll)
-  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
-  | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
-
-  (* Conversion *)
-  | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
-  | TacChange (op,c,cl) ->
-      TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
-        subst_glob_constr subst c, cl)
-
-  (* Equivalence relations *)
-  | TacReflexivity | TacSymmetry _ as x -> x
-  | TacTransitivity c -> TacTransitivity (Option.map (subst_glob_constr subst) c)
-
-  (* Equality and inversion *)
-  | TacRewrite (ev,l,cl,by) ->
-      TacRewrite (ev,
-		  List.map (fun (b,m,c) ->
-			      b,m,subst_glob_with_bindings subst c) l,
-		 cl,Option.map (subst_tactic subst) by)
-  | TacInversion (DepInversion (k,c,l),hyp) ->
-     TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp)
-  | TacInversion (NonDepInversion _,_) as x -> x
-  | TacInversion (InversionUsing (c,cl),hyp) ->
-      TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp)
-
-  (* For extensions *)
-  | TacExtend (_loc,opn,l) ->
-      TacExtend (dloc,opn,List.map (subst_genarg subst) l)
-  | TacAlias (_,s,l,(dir,body)) ->
-      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,
-        (dir,subst_tactic subst body))
-
-and subst_tactic subst (t:glob_tactic_expr) = match t with
-  | TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
-  | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
-  | TacLetIn (r,l,u) ->
-      let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in
-      TacLetIn (r,l,subst_tactic subst u)
-  | TacMatchGoal (lz,lr,lmr) ->
-      TacMatchGoal(lz,lr, subst_match_rule subst lmr)
-  | TacMatch (lz,c,lmr) ->
-      TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr)
-  | TacId _ | TacFail _ as x -> x
-  | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
-  | TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr)
-  | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
-  | TacThen (t1,tf,t2,tl) ->
-      TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
-	       subst_tactic subst t2,Array.map (subst_tactic subst) tl)
-  | TacThens (t,tl) ->
-      TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
-  | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
-  | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac)
-  | TacTry tac -> TacTry (subst_tactic subst tac)
-  | TacInfo tac -> TacInfo (subst_tactic subst tac)
-  | TacRepeat tac -> TacRepeat (subst_tactic subst tac)
-  | TacOrelse (tac1,tac2) ->
-      TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2)
-  | TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
-  | TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
-  | TacComplete tac -> TacComplete (subst_tactic subst tac)
-  | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a)
-
-and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
-
-and subst_tacarg subst = function
-  | Reference r -> Reference (subst_reference subst r)
-  | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
-  | MetaIdArg (_loc,_,_) -> assert false
-  | TacCall (_loc,f,l) ->
-      TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
-  | TacExternal (_loc,com,req,la) ->
-      TacExternal (_loc,com,req,List.map (subst_tacarg subst) la)
-  | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x
-  | Tacexp t -> Tacexp (subst_tactic subst t)
-  | TacDynamic(the_loc,t) as x ->
-      (match Dyn.tag t with
-	| "tactic" | "value" -> x
-        | "constr" ->
-          TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t)))
-	| s -> anomaly_loc (dloc, "Tacinterp.val_interp",
-                 str "Unknown dynamic: <" ++ str s ++ str ">"))
-
-(* Reads the rules of a Match Context or a Match *)
-and subst_match_rule subst = function
-  | (All tc)::tl ->
-      (All (subst_tactic subst tc))::(subst_match_rule subst tl)
-  | (Pat (rl,mp,tc))::tl ->
-      let hyps = subst_match_goal_hyps subst rl in
-      let pat = subst_match_pattern subst mp in
-      Pat (hyps,pat,subst_tactic subst tc)
-      ::(subst_match_rule subst tl)
-  | [] -> []
-
-and subst_genarg subst (x:glob_generic_argument) =
-  match genarg_tag x with
-  | BoolArgType -> in_gen globwit_bool (out_gen globwit_bool x)
-  | IntArgType -> in_gen globwit_int (out_gen globwit_int x)
-  | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x)
-  | StringArgType -> in_gen globwit_string (out_gen globwit_string x)
-  | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x)
-  | IntroPatternArgType ->
-      in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
-  | IdentArgType b ->
-      in_gen (globwit_ident_gen b) (out_gen (globwit_ident_gen b) x)
-  | VarArgType -> in_gen globwit_var (out_gen globwit_var x)
-  | RefArgType ->
-      in_gen globwit_ref (subst_global_reference subst
-	(out_gen globwit_ref x))
-  | SortArgType ->
-      in_gen globwit_sort (out_gen globwit_sort x)
-  | ConstrArgType ->
-      in_gen globwit_constr (subst_glob_constr subst (out_gen globwit_constr x))
-  | ConstrMayEvalArgType ->
-      in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
-  | QuantHypArgType ->
-      in_gen globwit_quant_hyp
-        (subst_declared_or_quantified_hypothesis subst
-          (out_gen globwit_quant_hyp x))
-  | RedExprArgType ->
-      in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
-  | OpenConstrArgType b ->
-      in_gen (globwit_open_constr_gen b)
-        ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen b) x)))
-  | ConstrWithBindingsArgType ->
-      in_gen globwit_constr_with_bindings
-        (subst_glob_with_bindings subst (out_gen globwit_constr_with_bindings x))
-  | BindingsArgType ->
-      in_gen globwit_bindings
-        (subst_bindings subst (out_gen globwit_bindings x))
-  | List0ArgType _ -> app_list0 (subst_genarg subst) x
-  | List1ArgType _ -> app_list1 (subst_genarg subst) x
-  | OptArgType _ -> app_opt (subst_genarg subst) x
-  | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
-  | ExtraArgType s ->
-      match tactic_genarg_level s with
-      | Some n ->
-          (* Special treatment of tactic arguments *)
-          in_gen (globwit_tactic n)
-            (subst_tactic subst (out_gen (globwit_tactic n) x))
-      | None ->
-          lookup_genarg_subst s subst x
-
-(***************************************************************************)
-(* Tactic registration *)
-
-(* Declaration of the TAC-DEFINITION object *)
-let add (kn,td) = mactab := Gmap.add kn td !mactab
-let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
-
-type tacdef_kind = | NewTac of identifier
-		   | UpdateTac of ltac_constant
-
-let load_md i ((sp,kn),(local,defs)) =
-  let dp,_ = repr_path sp in
-  let mp,dir,_ = repr_kn kn in
-  List.iter (fun (id,t) ->
-    match id with
-	NewTac id ->
-	  let sp = Libnames.make_path dp id in
-	  let kn = Names.make_kn mp dir (label_of_id id) in
-	    Nametab.push_tactic (Until i) sp kn;
-	    add (kn,t)
-      | UpdateTac kn -> replace (kn,t)) defs
-
-let open_md i ((sp,kn),(local,defs)) =
-  let dp,_ = repr_path sp in
-  let mp,dir,_ = repr_kn kn in
-  List.iter (fun (id,t) ->
-    match id with
-	NewTac id ->
-	  let sp = Libnames.make_path dp id in
-	  let kn = Names.make_kn mp dir (label_of_id id) in
-	    Nametab.push_tactic (Exactly i) sp kn
-      | UpdateTac kn -> ()) defs
-
-let cache_md x = load_md 1 x
-
-let subst_kind subst id =
-  match id with
-    | NewTac _ -> id
-    | UpdateTac kn -> UpdateTac (subst_kn subst kn)
-
-let subst_md (subst,(local,defs)) =
-  (local,
-   List.map (fun (id,t) -> (subst_kind subst id,subst_tactic subst t)) defs)
-
-let classify_md (local,defs as o) =
-  if local then Dispose else Substitute o
-
-let inMD : bool * (tacdef_kind * glob_tactic_expr) list -> obj =
-  declare_object {(default_object "TAC-DEFINITION") with
-     cache_function  = cache_md;
-     load_function   = load_md;
-     open_function   = open_md;
-     subst_function = subst_md;
-     classify_function = classify_md}
-
-let split_ltac_fun = function
-  | TacFun (l,t) -> (l,t)
-  | t -> ([],t)
-
-let pr_ltac_fun_arg = function
-  | None -> spc () ++ str "_"
-  | Some id -> spc () ++ pr_id id
-
-let print_ltac id =
- try
-  let kn = Nametab.locate_tactic id in
-  let l,t = split_ltac_fun (lookup kn) in
-  hv 2 (
-    hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
-           prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
-    ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t)
- with
-  Not_found ->
-   errorlabstrm "print_ltac"
-    (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
-
-open Libnames
-
-(* Adds a definition for tactics in the table *)
-let make_absolute_name ident repl =
-  let loc = loc_of_reference ident in
-  try
-    let id, kn =
-      if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident))
-      else let id = coerce_reference_to_id ident in
-	     Some id, Lib.make_kn id
-    in
-      if Gmap.mem kn !mactab then
-	if repl then id, kn
-	else
-	  user_err_loc (loc,"Tacinterp.add_tacdef",
-		       str "There is already an Ltac named " ++ pr_reference ident ++ str".")
-      else if is_atomic_kn kn then
-	user_err_loc (loc,"Tacinterp.add_tacdef",
-		     str "Reserved Ltac name " ++ pr_reference ident ++ str".")
-      else id, kn
-  with Not_found ->
-    user_err_loc (loc,"Tacinterp.add_tacdef",
-		 str "There is no Ltac named " ++ pr_reference ident ++ str".")
-
-let add_tacdef local isrec tacl =
-  let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in
-  let ist =
-    {(make_empty_glob_sign()) with ltacrecvars =
-	if isrec then List.map_filter
-	  (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun
-	else []} in
-  let gtacl =
-    List.map2 (fun (_,b,def) (id, qid) ->
-      let k = if b then UpdateTac qid else NewTac (Option.get id) in
-      let t = Flags.with_option strict_check (intern_tactic_or_tacarg ist) def in
-	(k, t))
-      tacl rfun in
-  let id0 = fst (List.hd rfun) in
-  let _ = match id0 with
-    | Some id0 -> ignore(Lib.add_leaf id0 (inMD (local,gtacl)))
-    | _ -> Lib.add_anonymous_leaf (inMD (local,gtacl)) in
-  List.iter
-    (fun (id,b,_) ->
-      Flags.if_verbose msg_info (Libnames.pr_reference id ++
-				 (if b then str " is redefined"
-				   else str " is defined")))
-    tacl
 
 (***************************************************************************)
 (* Other entry points *)
 
-let glob_tactic x =
-  Flags.with_option strict_check (intern_tactic true (make_empty_glob_sign ())) x
-
-let glob_tactic_env l env x =
-  Flags.with_option strict_check
-  (intern_pure_tactic
-    { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
-    x
-
 let interp_redexp env sigma r =
   let ist = { lfun=[]; avoid_ids=[]; debug=get_debug (); trace=[] } in
-  let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = sigma } in
+  let gist = { fully_empty_glob_sign with genv = env; gsigma = sigma } in
   interp_red_expr ist sigma env (intern_red_expr gist r)
 
 (***************************************************************************)
@@ -3194,8 +1962,3 @@ let _ = Auto.set_extern_interp
   (fun l ->
     let l = List.map (fun (id,c) -> (id,VConstr ([],c))) l in
     interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]})
-let _ = Auto.set_extern_intern_tac
-  (fun l ->
-    Flags.with_option strict_check
-    (intern_pure_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
-let _ = Auto.set_extern_subst_tactic subst_tactic
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 32e430d6ae..1401bab4ea 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -56,64 +56,16 @@ val set_debug : debug_info -> unit
 (** Gives the state of debug *)
 val get_debug : unit -> debug_info
 
-(** Adds a definition for tactics in the table *)
-val add_tacdef :
-  Vernacexpr.locality_flag -> bool ->
-  (Libnames.reference * bool * raw_tactic_expr) list -> unit
-val add_primitive_tactic : string -> glob_tactic_expr -> unit
-
-(** Tactic extensions *)
-val add_tactic :
-  string -> (typed_generic_argument list -> tactic) -> unit
-val overwriting_add_tactic :
-  string -> (typed_generic_argument list -> tactic) -> unit
-val lookup_tactic :
-  string -> (typed_generic_argument list) -> tactic
 
 (** Adds an interpretation function for extra generic arguments *)
-type glob_sign = {
-  ltacvars : identifier list * identifier list;
-  ltacrecvars : (identifier * Nametab.ltac_constant) list;
-  gsigma : Evd.evar_map;
-  genv : Environ.env }
 
-val fully_empty_glob_sign : glob_sign
+type interp_genarg_type =
+    interp_sign -> goal sigma -> glob_generic_argument ->
+      Evd.evar_map * typed_generic_argument
 
-val add_interp_genarg :
-  string ->
-    (glob_sign -> raw_generic_argument -> glob_generic_argument) *
-    (interp_sign -> goal sigma -> glob_generic_argument ->
-      Evd.evar_map * typed_generic_argument) *
-    (substitution -> glob_generic_argument -> glob_generic_argument)
-    -> unit
+val add_interp_genarg : string -> interp_genarg_type -> unit
 
-val interp_genarg :
-  interp_sign -> goal sigma -> glob_generic_argument -> Evd.evar_map * typed_generic_argument
-
-val intern_genarg :
-  glob_sign -> raw_generic_argument -> glob_generic_argument
-
-val intern_pure_tactic :
-  glob_sign -> raw_tactic_expr -> glob_tactic_expr
-
-val intern_constr :
-  glob_sign -> constr_expr -> glob_constr_and_expr
-
-val intern_constr_with_bindings :
-  glob_sign -> constr_expr * constr_expr bindings ->
-  glob_constr_and_expr * glob_constr_and_expr bindings
-
-val intern_hyp :
-  glob_sign -> identifier Loc.located -> identifier Loc.located
-
-val subst_genarg :
-  substitution -> glob_generic_argument -> glob_generic_argument
-
-val subst_glob_constr_and_expr :
-  substitution -> glob_constr_and_expr -> glob_constr_and_expr
-
-val subst_glob_with_bindings :
-  substitution -> glob_constr_and_expr with_bindings -> glob_constr_and_expr with_bindings
+val interp_genarg : interp_genarg_type
 
 (** Interprets any expression *)
 val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value
@@ -123,12 +75,9 @@ val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr ->
   Evd.evar_map * constr
 
 (** Interprets redexp arguments *)
-val dump_glob_red_expr : raw_red_expr -> unit
 val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr
 
 (** Interprets tactic expressions *)
-val interp_tac_gen : (identifier * value) list -> identifier list ->
-                 debug_info -> raw_tactic_expr -> tactic
 
 val interp_hyp :  interp_sign -> goal sigma -> identifier Loc.located -> identifier
 
@@ -139,18 +88,18 @@ val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_ma
   glob_constr_and_expr with_bindings -> Evd.evar_map * constr with_bindings
 
 (** Initial call for interpretation *)
-val glob_tactic : raw_tactic_expr -> glob_tactic_expr
-
-val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
 
 val eval_tactic : glob_tactic_expr -> tactic
 
+(** Globalization + interpretation *)
+
+val interp_tac_gen : (identifier * value) list -> identifier list ->
+                 debug_info -> raw_tactic_expr -> tactic
+
 val interp : raw_tactic_expr -> tactic
 
 val eval_ltac_constr : goal sigma -> raw_tactic_expr -> Evd.evar_map * constr
 
-val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
-
 (** Hides interpretation for pretty-print *)
 
 val hide_interp : raw_tactic_expr -> tactic option -> tactic
@@ -159,9 +108,6 @@ val hide_interp : raw_tactic_expr -> tactic option -> tactic
 val declare_xml_printer :
   (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit
 
-(** printing *)
-val print_ltac : Libnames.qualid -> std_ppcmds
-
 (** Internals that can be useful for syntax extensions. *)
 
 exception CannotCoerceTo of string
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
new file mode 100644
index 0000000000..42f1424422
--- /dev/null
+++ b/tactics/tacsubst.ml
@@ -0,0 +1,348 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Tacexpr
+open Mod_subst
+open Genarg
+open Misctypes
+open Globnames
+open Term
+open Genredexpr
+open Inductiveops
+open Patternops
+open Pretyping
+
+(** Substitution of tactics at module closing time *)
+
+(** 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 (Stringmap.empty : subst_genarg_type Stringmap.t)
+let add_genarg_subst id f =
+  genargsubs := Stringmap.add id f !genargsubs
+let lookup_genarg_subst id =
+  try Stringmap.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
+
+let subst_glob_constr_and_expr subst (c,e) =
+  assert (e=None); (* e<>None only for toplevel tactics *)
+  (Detyping.subst_glob_constr subst c,None)
+
+let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
+
+let subst_binding subst (loc,b,c) =
+  (loc,subst_quantified_hypothesis subst b,subst_glob_constr subst c)
+
+let subst_bindings subst = function
+  | NoBindings -> NoBindings
+  | ImplicitBindings l -> ImplicitBindings (List.map (subst_glob_constr subst) l)
+  | ExplicitBindings l -> ExplicitBindings (List.map (subst_binding subst) l)
+
+let subst_glob_with_bindings subst (c,bl) =
+  (subst_glob_constr subst c, subst_bindings subst bl)
+
+let subst_induction_arg subst = function
+  | ElimOnConstr c -> ElimOnConstr (subst_glob_with_bindings subst c)
+  | ElimOnAnonHyp n as x -> x
+  | ElimOnIdent id as x -> x
+
+let subst_and_short_name f (c,n) =
+(*  assert (n=None); *)(* since tacdef are strictly globalized *)
+  (f c,None)
+
+let subst_or_var f =  function
+  | ArgVar _ as x -> x
+  | ArgArg x -> ArgArg (f x)
+
+let dloc = Loc.ghost
+
+let subst_located f (_loc,id) = (dloc,f id)
+
+let subst_reference subst =
+  subst_or_var (subst_located (subst_kn subst))
+
+(*CSC: subst_global_reference is used "only" for RefArgType, that propagates
+  to the syntactic non-terminals "global", used in commands such as
+  Print. It is also used for non-evaluable references. *)
+open Pp
+open Printer
+
+let subst_global_reference subst =
+ let subst_global ref =
+  let ref',t' = subst_global subst ref in
+   if not (eq_constr (constr_of_global ref') t') then
+    msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
+          str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
+          pr_global ref') ;
+   ref'
+ in
+  subst_or_var (subst_located subst_global)
+
+let subst_evaluable subst =
+  let subst_eval_ref = subst_evaluable_reference subst in
+    subst_or_var (subst_and_short_name subst_eval_ref)
+
+let subst_unfold subst (l,e) =
+  (l,subst_evaluable subst e)
+
+let subst_flag subst red =
+  { red with rConst = List.map (subst_evaluable subst) red.rConst }
+
+let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
+
+let subst_glob_constr_or_pattern subst (c,p) =
+  (subst_glob_constr subst c,subst_pattern subst p)
+
+let subst_pattern_with_occurrences subst (l,p) =
+  (l,subst_glob_constr_or_pattern subst p)
+
+let subst_redexp subst = function
+  | Unfold l -> Unfold (List.map (subst_unfold subst) l)
+  | Fold l -> Fold (List.map (subst_glob_constr subst) l)
+  | Cbv f -> Cbv (subst_flag subst f)
+  | Lazy f -> Lazy (subst_flag subst f)
+  | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
+  | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o)
+  | CbvVm o -> CbvVm (Option.map (subst_pattern_with_occurrences subst) o)
+  | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
+
+let subst_raw_may_eval subst = function
+  | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c)
+  | ConstrContext (locid,c) -> ConstrContext (locid,subst_glob_constr subst c)
+  | ConstrTypeOf c -> ConstrTypeOf (subst_glob_constr subst c)
+  | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c)
+
+let subst_match_pattern subst = function
+  | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc))
+  | Term pc -> Term (subst_glob_constr_or_pattern subst pc)
+
+let rec subst_match_goal_hyps subst = function
+  | Hyp (locs,mp) :: tl ->
+      Hyp (locs,subst_match_pattern subst mp)
+      :: subst_match_goal_hyps subst tl
+  | Def (locs,mv,mp) :: tl ->
+      Def (locs,subst_match_pattern subst mv, subst_match_pattern subst mp)
+      :: subst_match_goal_hyps subst tl
+  | [] -> []
+
+let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
+  (* Basic tactics *)
+  | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
+  | TacAssumption as x -> x
+  | TacExact c -> TacExact (subst_glob_constr subst c)
+  | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c)
+  | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c)
+  | TacApply (a,ev,cb,cl) ->
+      TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl)
+  | TacElim (ev,cb,cbo) ->
+      TacElim (ev,subst_glob_with_bindings subst cb,
+               Option.map (subst_glob_with_bindings subst) cbo)
+  | TacElimType c -> TacElimType (subst_glob_constr subst c)
+  | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb)
+  | TacCaseType c -> TacCaseType (subst_glob_constr subst c)
+  | TacFix (idopt,n) as x -> x
+  | TacMutualFix (id,n,l) ->
+      TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
+  | TacCofix idopt as x -> x
+  | TacMutualCofix (id,l) ->
+      TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
+  | TacCut c -> TacCut (subst_glob_constr subst c)
+  | TacAssert (b,na,c) ->
+      TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
+  | TacGeneralize cl ->
+      TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
+  | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c)
+  | TacLetTac (id,c,clp,b,eqpat) ->
+    TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat)
+
+  (* Automation tactics *)
+  | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
+  | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
+
+  (* Derived basic tactics *)
+  | TacSimpleInductionDestruct (isrec,h) as x -> x
+  | TacInductionDestruct (isrec,ev,(l,el,cls)) ->
+      let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in
+      let el' = Option.map (subst_glob_with_bindings subst) el in
+      TacInductionDestruct (isrec,ev,(l',el',cls))
+  | TacDoubleInduction (h1,h2) as x -> x
+  | TacDecomposeAnd c -> TacDecomposeAnd (subst_glob_constr subst c)
+  | TacDecomposeOr c -> TacDecomposeOr (subst_glob_constr subst c)
+  | TacDecompose (l,c) ->
+      let l = List.map (subst_or_var (subst_inductive subst)) l in
+      TacDecompose (l,subst_glob_constr subst c)
+  | TacSpecialize (n,l) -> TacSpecialize (n,subst_glob_with_bindings subst l)
+  | TacLApply c -> TacLApply (subst_glob_constr subst c)
+
+  (* Context management *)
+  | TacClear _ as x -> x
+  | TacClearBody l as x -> x
+  | TacMove (dep,id1,id2) as x -> x
+  | TacRename l as x -> x
+  | TacRevert _ as x -> x
+
+  (* Constructors *)
+  | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl)
+  | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl)
+  | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (subst_bindings subst) bll)
+  | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t)
+  | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl)
+
+  (* Conversion *)
+  | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
+  | TacChange (op,c,cl) ->
+      TacChange (Option.map (subst_glob_constr_or_pattern subst) op,
+        subst_glob_constr subst c, cl)
+
+  (* Equivalence relations *)
+  | TacReflexivity | TacSymmetry _ as x -> x
+  | TacTransitivity c -> TacTransitivity (Option.map (subst_glob_constr subst) c)
+
+  (* Equality and inversion *)
+  | TacRewrite (ev,l,cl,by) ->
+      TacRewrite (ev,
+		  List.map (fun (b,m,c) ->
+			      b,m,subst_glob_with_bindings subst c) l,
+		 cl,Option.map (subst_tactic subst) by)
+  | TacInversion (DepInversion (k,c,l),hyp) ->
+     TacInversion (DepInversion (k,Option.map (subst_glob_constr subst) c,l),hyp)
+  | TacInversion (NonDepInversion _,_) as x -> x
+  | TacInversion (InversionUsing (c,cl),hyp) ->
+      TacInversion (InversionUsing (subst_glob_constr subst c,cl),hyp)
+
+  (* For extensions *)
+  | TacExtend (_loc,opn,l) ->
+      TacExtend (dloc,opn,List.map (subst_genarg subst) l)
+  | TacAlias (_,s,l,(dir,body)) ->
+      TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,
+        (dir,subst_tactic subst body))
+
+and subst_tactic subst (t:glob_tactic_expr) = match t with
+  | TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
+  | TacFun tacfun -> TacFun (subst_tactic_fun subst tacfun)
+  | TacLetIn (r,l,u) ->
+      let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in
+      TacLetIn (r,l,subst_tactic subst u)
+  | TacMatchGoal (lz,lr,lmr) ->
+      TacMatchGoal(lz,lr, subst_match_rule subst lmr)
+  | TacMatch (lz,c,lmr) ->
+      TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr)
+  | TacId _ | TacFail _ as x -> x
+  | TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
+  | TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr)
+  | TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
+  | TacThen (t1,tf,t2,tl) ->
+      TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
+	       subst_tactic subst t2,Array.map (subst_tactic subst) tl)
+  | TacThens (t,tl) ->
+      TacThens (subst_tactic subst t, List.map (subst_tactic subst) tl)
+  | TacDo (n,tac) -> TacDo (n,subst_tactic subst tac)
+  | TacTimeout (n,tac) -> TacTimeout (n,subst_tactic subst tac)
+  | TacTry tac -> TacTry (subst_tactic subst tac)
+  | TacInfo tac -> TacInfo (subst_tactic subst tac)
+  | TacRepeat tac -> TacRepeat (subst_tactic subst tac)
+  | TacOrelse (tac1,tac2) ->
+      TacOrelse (subst_tactic subst tac1,subst_tactic subst tac2)
+  | TacFirst l -> TacFirst (List.map (subst_tactic subst) l)
+  | TacSolve l -> TacSolve (List.map (subst_tactic subst) l)
+  | TacComplete tac -> TacComplete (subst_tactic subst tac)
+  | TacArg (_,a) -> TacArg (dloc,subst_tacarg subst a)
+
+and subst_tactic_fun subst (var,body) = (var,subst_tactic subst body)
+
+and subst_tacarg subst = function
+  | Reference r -> Reference (subst_reference subst r)
+  | ConstrMayEval c -> ConstrMayEval (subst_raw_may_eval subst c)
+  | MetaIdArg (_loc,_,_) -> assert false
+  | TacCall (_loc,f,l) ->
+      TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l)
+  | TacExternal (_loc,com,req,la) ->
+      TacExternal (_loc,com,req,List.map (subst_tacarg subst) la)
+  | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x
+  | Tacexp t -> Tacexp (subst_tactic subst t)
+  | TacDynamic(the_loc,t) as x ->
+      (match Dyn.tag t with
+	| "tactic" | "value" -> x
+        | "constr" ->
+          TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t)))
+	| s -> Errors.anomaly_loc (dloc, "Tacinterp.val_interp",
+                 str "Unknown dynamic: <" ++ str s ++ str ">"))
+
+(* Reads the rules of a Match Context or a Match *)
+and subst_match_rule subst = function
+  | (All tc)::tl ->
+      (All (subst_tactic subst tc))::(subst_match_rule subst tl)
+  | (Pat (rl,mp,tc))::tl ->
+      let hyps = subst_match_goal_hyps subst rl in
+      let pat = subst_match_pattern subst mp in
+      Pat (hyps,pat,subst_tactic subst tc)
+      ::(subst_match_rule subst tl)
+  | [] -> []
+
+and subst_genarg subst (x:glob_generic_argument) =
+  match genarg_tag x with
+  | BoolArgType -> in_gen globwit_bool (out_gen globwit_bool x)
+  | IntArgType -> in_gen globwit_int (out_gen globwit_int x)
+  | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x)
+  | StringArgType -> in_gen globwit_string (out_gen globwit_string x)
+  | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x)
+  | IntroPatternArgType ->
+      in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
+  | IdentArgType b ->
+      in_gen (globwit_ident_gen b) (out_gen (globwit_ident_gen b) x)
+  | VarArgType -> in_gen globwit_var (out_gen globwit_var x)
+  | RefArgType ->
+      in_gen globwit_ref (subst_global_reference subst
+	(out_gen globwit_ref x))
+  | SortArgType ->
+      in_gen globwit_sort (out_gen globwit_sort x)
+  | ConstrArgType ->
+      in_gen globwit_constr (subst_glob_constr subst (out_gen globwit_constr x))
+  | ConstrMayEvalArgType ->
+      in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
+  | QuantHypArgType ->
+      in_gen globwit_quant_hyp
+        (subst_declared_or_quantified_hypothesis subst
+          (out_gen globwit_quant_hyp x))
+  | RedExprArgType ->
+      in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
+  | OpenConstrArgType b ->
+      in_gen (globwit_open_constr_gen b)
+        ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen b) x)))
+  | ConstrWithBindingsArgType ->
+      in_gen globwit_constr_with_bindings
+        (subst_glob_with_bindings subst (out_gen globwit_constr_with_bindings x))
+  | BindingsArgType ->
+      in_gen globwit_bindings
+        (subst_bindings subst (out_gen globwit_bindings x))
+  | List0ArgType _ -> app_list0 (subst_genarg subst) x
+  | List1ArgType _ -> app_list1 (subst_genarg subst) x
+  | 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 (Extrawit.globwit_tactic n)
+            (subst_tactic subst (out_gen (Extrawit.globwit_tactic n) x))
+      | None ->
+          lookup_genarg_subst s subst x
+
+let _ = Auto.set_extern_subst_tactic subst_tactic
diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli
new file mode 100644
index 0000000000..ade3e7cc91
--- /dev/null
+++ b/tactics/tacsubst.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Tacexpr
+open Mod_subst
+open Genarg
+open Misctypes
+
+(** Substitution of tactics at module closing time *)
+
+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
+
+(** Misc *)
+
+val subst_glob_constr_and_expr :
+  substitution -> glob_constr_and_expr -> glob_constr_and_expr
+
+val subst_glob_with_bindings : substitution ->
+  glob_constr_and_expr with_bindings ->
+  glob_constr_and_expr with_bindings
diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml
index 7989b41db8..5614858335 100644
--- a/tactics/tactic_option.ml
+++ b/tactics/tactic_option.ml
@@ -22,7 +22,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
     if not local then set_default_tactic local tac
   in
   let subst (s, (local, tac)) =
-    (local, Tacinterp.subst_tactic s tac)
+    (local, Tacsubst.subst_tactic s tac)
   in
   let input : bool * Tacexpr.glob_tactic_expr -> obj =
     declare_object
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 9e5fbcc7c8..7a3eae2679 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -16,6 +16,8 @@ Contradiction
 Refine
 Inv
 Leminv
+Tacsubst
+Tacintern
 Tacinterp
 Evar_tactics
 Autorewrite
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e7c19fbb21..ed6b452282 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -73,7 +73,7 @@ let cache_tactic_notation (_, tobj) =
 
 let subst_tactic_parule subst tg =
   let dir, tac = tg.tacgram_tactic in
-  { tg with tacgram_tactic = (dir, Tacinterp.subst_tactic subst tac); }
+  { tg with tacgram_tactic = (dir, Tacsubst.subst_tactic subst tac); }
 
 let subst_tactic_notation (subst, tobj) =
   { tobj with
@@ -112,7 +112,7 @@ let add_tactic_notation (local,n,prods,e) =
     pptac_prods = (n, List.map make_terminal_status prods);
   } in
   let ids = List.fold_left cons_production_parameter [] prods in
-  let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in
+  let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
   let parule = {
     tacgram_key = key;
     tacgram_level = n;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 016f0c60af..fa00689982 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -876,7 +876,7 @@ let vernac_restore_state file =
 (* Commands *)
 
 let vernac_declare_tactic_definition (local,x,def) =
-  Tacinterp.add_tacdef local x def
+  Tacintern.add_tacdef local x def
 
 let vernac_create_hintdb local id b =
   Auto.create_hint_db local id full_transparent_state b
@@ -1317,7 +1317,7 @@ let vernac_check_may_eval redexp glopt rc =
     | None ->
 	msg_notice (print_judgment env j)
     | Some r ->
-        Tacinterp.dump_glob_red_expr r;
+        Tacintern.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in
 	let redfun = fst (reduction_of_red_expr r_interp) in
 	msg_notice (print_eval redfun env sigma' rc j)
@@ -1352,7 +1352,7 @@ let vernac_print = function
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
-  | PrintLtac qid -> msg_notice (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
+  | PrintLtac qid -> msg_notice (Tacintern.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> msg_notice (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))