Moving Tacinterp to Hightactics.

7 files changed, 15 insertions, 8 deletions

diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
index eed6caea30..8df519b567 100644
--- a/parsing/highparsing.mllib
+++ b/parsing/highparsing.mllib
@@ -3,4 +3,3 @@ G_vernac
 G_prim
 G_proofs
 G_tactic
-G_ltac
diff --git a/parsing/g_ltac.ml4 b/tactics/g_ltac.ml4
index d1992c57bb..d1992c57bb 100644
--- a/parsing/g_ltac.ml4
+++ b/tactics/g_ltac.ml4
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 5c59465429..0649f2f72e 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,3 +1,6 @@
+Tacinterp
+Evar_tactics
+Tactic_option
 Extraargs
 G_obligations
 Coretactics
@@ -12,3 +15,4 @@ G_rewrite
 Tauto
 Eqdecide
 G_eqdecide
+G_ltac
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 36faba1137..6bf0e2aa73 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2214,3 +2214,5 @@ let _ =
       optkey   = ["Ltac";"Debug"];
       optread  = (fun () -> get_debug () != Tactic_debug.DebugOff);
       optwrite = vernac_debug }
+
+let () = Hook.set Vernacentries.interp_redexp_hook interp_redexp
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index fd7fab0c58..584cc0b730 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -22,7 +22,4 @@ Auto
 Tacintern
 Tactic_matching
 Tactic_debug
-Tacinterp
-Evar_tactics
 Term_dnet
-Tactic_option
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8ba5eb3f7d..64f9cd9caa 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -20,7 +20,6 @@ open Tacmach
 open Constrintern
 open Prettyp
 open Printer
-open Tacinterp
 open Command
 open Goptions
 open Libnames
@@ -34,6 +33,9 @@ open Misctypes
 open Locality
 open Sigma.Notations
 
+(** TODO: make this function independent of Ltac *)
+let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
+
 let debug = false
 let prerr_endline =
   if debug then prerr_endline else fun _ -> ()
@@ -471,7 +473,7 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
           | None -> None
           | Some r ->
 	      let (evc,env)= get_current_context () in
- 		Some (snd (interp_redexp env evc r)) in
+ 		Some (snd (Hook.get f_interp_redexp env evc r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof locality p kind l lettop =
@@ -1501,7 +1503,7 @@ let vernac_check_may_eval redexp glopt rc =
                     Printer.pr_universe_ctx sigma uctx)
     | Some r ->
         Tacintern.dump_glob_red_expr r;
-        let (sigma',r_interp) = interp_redexp env sigma' r in
+        let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in
 	let redfun env evm c =
           let (redfun, _) = reduction_of_red_expr env r_interp in
           let evm = Sigma.Unsafe.of_evar_map evm in
@@ -1512,7 +1514,7 @@ let vernac_check_may_eval redexp glopt rc =
 
 let vernac_declare_reduction locality s r =
   let local = make_locality locality in
-  declare_red_expr local s (snd (interp_redexp (Global.env()) Evd.empty r))
+  declare_red_expr local s (snd (Hook.get f_interp_redexp (Global.env()) Evd.empty r))
 
   (* The same but avoiding the current goal context if any *)
 let vernac_global_check c =
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4a59b1299b..4e7fa4a087 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -61,3 +61,6 @@ val vernac_end_proof :
 val with_fail : bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind
+
+val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr ->
+  Evd.evar_map * Redexpr.red_expr) Hook.t