Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR

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

1 files changed, 20 insertions, 4 deletions

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 0cdf49c70c..08446d0112 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -25,23 +25,39 @@ let db_pr_goal = function
   | Some g ->
     mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >]
 
+(* Prints the commands *)
+let help () =
+  mSGNL [< 'sTR "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit" >]
+
 (* Prints the state and waits for an instruction *)
 let debug_prompt goalopt tac_ast =
   db_pr_goal goalopt;
-  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL;
-         'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >];
+  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL >];
+(*         'sTR "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*)
+(*  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL;
+         'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >];*)
   let rec prompt () =
-    mSG [<'fNL; 'sTR "TcDebug> " >];
+    mSG [<'fNL; 'sTR "TcDebug > " >];
     flush stdout;
     let inst = read_line () in
-    mSGNL [<>];
+(*    mSGNL [<>];*)
     match inst with
     | ""  -> DebugOn
     | "s" -> DebugOff
     | "x" -> Exit
+    | "h" ->
+      begin
+        help ();
+        prompt ()
+      end
     | _   -> prompt () in
   prompt ()
 
+(* Prints a constr *)
+let db_constr debug env c =
+  if debug = DebugOn then
+    mSGNL [< 'sTR "Evaluated term --> ";  prterm_env env c >]
+
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,c) =
   if debug = DebugOn then