From 15daaa856a6dd1f97845c4f24fe27eaf4cdbdda0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 16 Oct 2012 16:24:23 +0000
Subject: 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
---
 toplevel/metasyntax.ml    | 4 ++--
 toplevel/vernacentries.ml | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'toplevel')

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))
-- 
cgit v1.2.3