From ae9f6d13b63f30168d2eaa2289108a117ad840f7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Sep 2016 18:51:52 +0200
Subject: Unplugging Tacexpr in several interface files.

---
 tactics/hints.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4b43a9e696..9ee9e798b1 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -24,7 +24,6 @@ open Evd
 open Termops
 open Inductiveops
 open Typing
-open Tacexpr
 open Decl_kinds
 open Pattern
 open Patternops
@@ -41,6 +40,8 @@ module NamedDecl = Context.Named.Declaration
 (* General functions                    *)
 (****************************************)
 
+type debug = Tacexpr.debug = Debug | Info | Off
+
 exception Bound
 
 let head_constr_bound t =
@@ -1093,7 +1094,7 @@ type hints_entry =
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
   | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * glob_tactic_expr
+      int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
 
 let default_prepare_hint_ident = Id.of_string "H"
 
@@ -1231,7 +1232,7 @@ let add_hint_lemmas env sigma eapply lems hint_db =
 let make_local_hint_db env sigma ts eapply lems =
   let map c =
     let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (c, sigma, _) = c.delayed env sigma in
+    let Sigma (c, sigma, _) = c.Pretyping.delayed env sigma in
     (Sigma.to_evar_map sigma, c)
   in
   let lems = List.map map lems in
-- 
cgit v1.2.3


From 1654b3989041b25e3b642ffde12125344342a54b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Sep 2016 20:37:24 +0200
Subject: Making Hints generic in the use of external tactics.

---
 tactics/hints.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9ee9e798b1..a6d1fc6c8e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -804,7 +804,6 @@ let make_unfold eref =
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
-  let tacast = Genarg.in_gen (Genarg.glbwit Constrarg.wit_ltac) tacast in
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
    { pri = pri;
@@ -1082,8 +1081,6 @@ let add_trivials env sigma l local dbnames =
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let (forward_intern_tac, extern_intern_tac) = Hook.make ()
-
 type hnf = bool
 
 type hints_entry =
@@ -1094,7 +1091,7 @@ type hints_entry =
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
   | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+      int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument
 
 let default_prepare_hint_ident = Id.of_string "H"
 
@@ -1184,7 +1181,9 @@ let interp_hints poly =
   | HintsExtern (pri, patcom, tacexp) ->
       let pat =	Option.map fp patcom in
       let l = match pat with None -> [] | Some (l, _) -> l in
-      let tacexp = Hook.get forward_intern_tac l tacexp in
+      let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
+      let env = Genintern.({ genv = env; ltacvars }) in
+      let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry (pri, pat, tacexp)
 
 let add_hints local dbnames0 h =
-- 
cgit v1.2.3


From 7045848145c16d978456aab2edd192c54d242e69 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 8 Sep 2016 14:43:46 +0200
Subject: Unplugging Pptactic from Ppvernac.

---
 tactics/hints.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index a6d1fc6c8e..4be4d1ed4b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1276,7 +1276,7 @@ let pr_hint h = match h.obj with
           env
         with e when CErrors.noncritical e -> Global.env ()
       in
-      (str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
+      (str "(*external*) " ++ Pputils.pr_glb_generic env tac)
 
 let pr_id_hint (id, v) =
   (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
-- 
cgit v1.2.3


From 72ac4b32ac26fdba751ae48568d28b4dbb8edd14 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 15 Sep 2016 18:11:54 +0200
Subject: Untangling Tacexpr from lower strata.

---
 tactics/hints.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics/hints.ml')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4be4d1ed4b..ac945de3c9 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -20,6 +20,7 @@ open Namegen
 open Libnames
 open Smartlocate
 open Misctypes
+open Tactypes
 open Evd
 open Termops
 open Inductiveops
@@ -40,7 +41,7 @@ module NamedDecl = Context.Named.Declaration
 (* General functions                    *)
 (****************************************)
 
-type debug = Tacexpr.debug = Debug | Info | Off
+type debug = Debug | Info | Off
 
 exception Bound
 
@@ -1231,7 +1232,7 @@ let add_hint_lemmas env sigma eapply lems hint_db =
 let make_local_hint_db env sigma ts eapply lems =
   let map c =
     let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (c, sigma, _) = c.Pretyping.delayed env sigma in
+    let Sigma (c, sigma, _) = c.delayed env sigma in
     (Sigma.to_evar_map sigma, c)
   in
   let lems = List.map map lems in
-- 
cgit v1.2.3