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

4 files changed, 10 insertions, 7 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)