From 2c13632cd7296072ab5271fc047cda720f23686c Mon Sep 17 00:00:00 2001
From: delahaye
Date: Mon, 30 Oct 2000 16:56:19 +0000
Subject: Tactiques utilisateur + debugger

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@786 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tactic_debug.mli | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 proofs/tactic_debug.mli

(limited to 'proofs/tactic_debug.mli')

diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
new file mode 100644
index 0000000000..26ab1a9470
--- /dev/null
+++ b/proofs/tactic_debug.mli
@@ -0,0 +1,21 @@
+open Proof_type
+open Term
+
+(* This module intends to be a beginning of debugger for tactic expressions.
+   Currently, it is quite simple and we can hope to have, in the future, a more
+   complete panel of commands dedicated to a proof assistant framework *)
+
+(* Debug information *)
+type debug_info =
+  | DebugOn
+  | DebugOff
+  | Exit
+
+(* Prints the state and waits *)
+val debug_prompt : goal sigma option -> Coqast.t -> debug_info
+
+(* Prints a matched hypothesis *)
+val db_matched_hyp : debug_info -> Environ.env -> string * constr -> unit
+
+(* Prints the matched conclusion *)
+val db_matched_concl : debug_info -> Environ.env -> constr -> unit
-- 
cgit v1.2.3