Tactiques utilisateur + debugger

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@786 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 22 insertions, 1 deletions

diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 746c89f08e..ee5d67966a 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -2,10 +2,12 @@
 (* $Id$ *)
 
 (*i*)
+open Dyn
 open Pp
 open Names
 open Proof_type
 open Tacmach
+open Tactic_debug
 open Term
 (*i*)
 
@@ -25,7 +27,26 @@ val constr_of_Constr : tactic_arg -> constr
 (* Signature for interpretation: [val_interp] and interpretation functions *)
 type interp_sign =
   enamed_declarations * Environ.env * (string * value) list * 
-    (int * constr) list * goal sigma option
+    (int * constr) list * goal sigma option * debug_info
+
+(* To provide the tactic expressions *)
+val loc : Coqast.loc
+val tacticIn : (unit -> Coqast.t) -> Coqast.t
+
+(* References for dynamic interpretation of user tactics. They are all
+   initialized with dummy values *)
+val r_evc     : enamed_declarations ref
+val r_env     : Environ.env ref
+val r_lfun    : (string * value) list ref
+val r_lmatch  : (int * constr) list ref
+val r_goalopt : goal sigma option ref
+val r_debug   : debug_info ref
+
+(* Sets the debugger mode *)
+val set_debug : debug_info -> unit
+
+(* Gives the state of debug *)
+val get_debug : unit -> debug_info
 
 (* Adds a Tactic Definition in the table *)
 val add_tacdef : string -> value -> unit