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

6 files changed, 26 insertions, 23 deletions

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