From 559dd3e37eab5023598eb3ef7cd0a86a3674ae8a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 7 Nov 2008 14:11:35 +0000
Subject: Add the ability to give a specific tactic to solve each obligation in
 Program. No syntax to do it yet.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11550 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 0d41db8a43..6faae3adc1 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -48,6 +48,9 @@ and interp_sign =
 val constr_of_id : Environ.env -> identifier -> constr
 
 (* To embed several objects in Coqast.t *)
+val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t
+val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)
+  
 val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
 val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr
 val valueIn : value -> raw_tactic_arg
-- 
cgit v1.2.3