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

1 files changed, 2 insertions, 2 deletions

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;