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

---
 proofs/pfedit.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/pfedit.mli')

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9b0200039..f2f4b11ed 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
-- 
cgit v1.2.3