From 5f703bbb8b4f439af9d76b1f6ef24162b67049c2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 02:43:45 +0100
Subject: Moving Tacintern to Hightactics.

---
 tactics/hightactics.mllib | 1 +
 tactics/tactics.mllib     | 1 -
 toplevel/vernacentries.ml | 1 -
 3 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index b18d148ec6..468b938b6a 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,3 +1,4 @@
+Tacintern
 Tacentries
 Tacinterp
 Evar_tactics
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 584cc0b730..b495a885f8 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -19,7 +19,6 @@ Taccoerce
 Tacenv
 Hints
 Auto
-Tacintern
 Tactic_matching
 Tactic_debug
 Term_dnet
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index bbfa8818b0..bdd52d5be0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1427,7 +1427,6 @@ let vernac_check_may_eval redexp glopt rc =
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
                     Printer.pr_universe_ctx sigma uctx)
     | Some r ->
-        Tacintern.dump_glob_red_expr r;
         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
-- 
cgit v1.2.3