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.

---
 proofs/clenvtac.mli   | 2 +-
 proofs/proof_type.mli | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index aa091aecda..8a096b6457 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -10,8 +10,8 @@
 
 open Term
 open Clenv
-open Tacexpr
 open Unification
+open Misctypes
 
 (** Tactics *)
 val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index f7798a0edb..ff60ae5bf7 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,7 +11,6 @@
 open Evd
 open Names
 open Term
-open Tacexpr
 open Glob_term
 open Nametab
 open Misctypes
-- 
cgit v1.2.3


From 52c3917be7239f7d5ab1ba882275b4571463f585 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 7 Sep 2016 23:59:08 +0200
Subject: Making Proof_global terminator generic in external tactics.

---
 proofs/pfedit.mli       |  2 +-
 proofs/proof_global.ml  | 13 ++++++++-----
 proofs/proof_global.mli |  5 +----
 3 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9b0200039b..f2f4b11ed3 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -124,7 +124,7 @@ val get_all_proof_names : unit -> Id.t list
 (** [set_end_tac tac] applies tactic [tac] to all subgoal generate
     by [solve] *)
 
-val set_end_tac : Tacexpr.raw_tactic_expr -> unit
+val set_end_tac : Genarg.glob_generic_argument -> unit
 
 (** {6 ... } *)
 (** [set_used_variables l] declares that section variables [l] will be
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f3ca19a903..2956d623fd 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -90,7 +90,7 @@ type closed_proof = proof_object * proof_terminator
 type pstate = {
   pid : Id.t;
   terminator : proof_terminator CEphemeron.key;
-  endline_tactic : Tacexpr.raw_tactic_expr option;
+  endline_tactic : Genarg.glob_generic_argument option;
   section_vars : Context.Named.t option;
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
@@ -148,9 +148,6 @@ let cur_pstate () =
 let give_me_the_proof () = (cur_pstate ()).proof
 let get_current_proof_name () = (cur_pstate ()).pid
 
-let interp_tac = ref (fun _ -> assert false)
-let set_interp_tac f = interp_tac := f
-
 let with_current_proof f =
   match !pstates with
   | [] -> raise NoCurrentProof
@@ -158,7 +155,13 @@ let with_current_proof f =
       let et =
         match p.endline_tactic with
         | None -> Proofview.tclUNIT ()
-        | Some tac -> !interp_tac tac in
+        | Some tac ->
+          let open Geninterp in
+          let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in
+          let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
+          let tac = Geninterp.interp tag ist tac in
+          Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
+      in
       let (newpr,ret) = f et p.proof in
       let p = { p with proof = newpr } in
       pstates := p :: rest;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 86fc1deff8..97a21cf225 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -134,10 +134,7 @@ val simple_with_current_proof :
   (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
 
 (** Sets the tactic to be used when a tactic line is closed with [...] *)
-val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit
-val set_interp_tac :
-  (Tacexpr.raw_tactic_expr -> unit Proofview.tactic)
-    -> unit
+val set_endline_tactic : Genarg.glob_generic_argument -> unit
 
 (** Sets the section variables assumed by the proof, returns its closure
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
-- 
cgit v1.2.3