Tactiques utilisateur + debugger

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

4 files changed, 301 insertions, 134 deletions

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 014dda7e7..98f2b3554 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -3,6 +3,7 @@
 
 open Astterm
 open Closure
+open Dyn
 (* open Generic *)
 open Libobject
 open Pattern
@@ -14,6 +15,7 @@ open Util
 open Names
 open Proof_type
 open Tacmach
+open Tactic_debug
 open Macros
 open Coqast
 open Ast
@@ -80,7 +82,33 @@ let rec constr_list goalopt = function
 (* 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
+
+(* For user tactics *)
+let ((ocamlIn : (unit -> Coqast.t) -> Dyn.t),
+     (ocamlOut : Dyn.t -> (unit -> Coqast.t))) = create "ocaml"
+
+(* To provide the tactic expressions *)
+let loc = (0,0)
+let tacticIn t = Dynamic (loc,ocamlIn t)
+
+(* References for dynamic interpretation of user tactics. They are all
+   initialized with dummy values *)
+let r_evc     = ref Evd.empty
+let r_env     = ref Environ.empty_env
+let r_lfun    = ref []
+let r_lmatch  = ref []
+let r_goalopt = ref None
+let r_debug   = ref DebugOn
+
+(* Updates the references with the current environment *)
+let env_update (evc,env,lfun,lmatch,goalopt,debug) =
+  r_evc     := evc;
+  r_env     := env;
+  r_lfun    := lfun;
+  r_lmatch  := lmatch;
+  r_goalopt := goalopt;
+  r_debug   := debug
 
 (* Table of interpretation functions *)
 let interp_tab =
@@ -362,75 +390,88 @@ let rec make_subs_list = function
   | e::tl -> make_subs_list tl
   | [] -> []
 
+(* Debug reference *)
+let debug =ref DebugOff
+
+(* Sets the debugger mode *)
+let set_debug pos = debug := pos
+
+(* Gives the state of debug *)
+let get_debug () = !debug
+
 (* Interprets any expression *)
-let rec val_interp (evc,env,lfun,lmatch,goalopt) ast =
+let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
 
 (* mSGNL [<print_ast ast>]; *)
 (* mSGNL [<print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)>] *)
 
+  let value_interp debug =
   match ast with
     | Node(_,"APP",l) ->
-      let fv = val_interp (evc,env,lfun,lmatch,goalopt) (List.hd l)
-      and largs = List.map (val_interp (evc,env,lfun,lmatch,goalopt)) (List.tl
-        l) in
-      app_interp evc env lfun lmatch goalopt fv largs ast
+      let fv = val_interp (evc,env,lfun,lmatch,goalopt,debug) (List.hd l)
+      and largs = List.map (val_interp (evc,env,lfun,lmatch,goalopt,debug))
+        (List.tl l) in
+      app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast
     | Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1)
-    | Node(_,"REC",l) -> rec_interp evc env lfun lmatch goalopt ast l
+    | Node(_,"REC",l) ->
+      rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast l
     | Node(_,"LET",[Node(_,"LETDECL",l);u]) ->
-      let addlfun=let_interp evc env lfun lmatch goalopt ast l in
-        val_interp (evc,env,(lfun@addlfun),lmatch,goalopt) u
+      let addlfun=let_interp (evc,env,lfun,lmatch,goalopt,debug) ast l in
+        val_interp (evc,env,(lfun@addlfun),lmatch,goalopt,debug) u
     | Node(_,"MATCHCONTEXT",lmr) ->
-      match_context_interp evc env lfun lmatch goalopt ast lmr
+      match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr
     | Node(_,"MATCH",lmr) ->
-      match_interp evc env lfun lmatch goalopt ast lmr
+      match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr
     | Node(_,"IDTAC",[]) -> VTactic tclIDTAC
     | Node(_,"FAIL",[]) -> VTactic (tclFAIL 0)
     | Node(_,"FAIL",[n]) -> VTactic (tclFAIL (num_of_ast n))
     | Node(_,"TACTICLIST",l) ->
-      VTactic (interp_semi_list tclIDTAC lfun lmatch l)
+      VTactic (interp_semi_list tclIDTAC lfun lmatch debug l)
     | Node(_,"DO",[n;tac]) ->
-      VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch tac))
+      VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch debug tac))
     | Node(_,"TRY",[tac]) ->
-      VTactic (tclTRY (tac_interp lfun lmatch tac))
+      VTactic (tclTRY (tac_interp lfun lmatch debug tac))
     | Node(_,"INFO",[tac]) ->
-      VTactic (tclINFO (tac_interp lfun lmatch tac))
+      VTactic (tclINFO (tac_interp lfun lmatch debug tac))
     | Node(_,"REPEAT",[tac]) ->
-      VTactic (tclREPEAT (tac_interp lfun lmatch tac))
+      VTactic (tclREPEAT (tac_interp lfun lmatch debug tac))
     | Node(_,"ORELSE",[tac1;tac2]) ->
-      VTactic (tclORELSE (tac_interp lfun lmatch tac1) (tac_interp lfun lmatch
-        tac2))
+      VTactic (tclORELSE (tac_interp lfun lmatch debug tac1)
+        (tac_interp lfun lmatch debug tac2))
     | Node(_,"FIRST",l) ->
-      VTactic (tclFIRST (List.map (tac_interp lfun lmatch) l))
+      VTactic (tclFIRST (List.map (tac_interp lfun lmatch debug) l))
     | Node(_,"TCLSOLVE",l) ->
-      VTactic (tclSOLVE (List.map (tac_interp lfun lmatch) l))
+      VTactic (tclSOLVE (List.map (tac_interp lfun lmatch debug) l))
     | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
-      val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc0,"APP",[Node(loc1,
-        "PRIM-TACTIC",[Node(loc1,s,[])])]@l))
+      val_interp (evc,env,lfun,lmatch,goalopt,debug)
+        (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))
     | Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) ->
       VFTactic ([],(interp_atomic loc opn))
     | Node(_,"VOID",[]) -> VVoid
     | Nvar(_,s) ->
-      (try (unrec (List.assoc s (List.rev lfun)))
+      (try (unrec (List.assoc s lfun))
        with | Not_found ->
          (try (lookup s)
           with | Not_found -> VArg (Identifier (id_of_string s))))
     | Str(_,s) -> VArg (Quoted_string s)
     | Num(_,n) -> VArg (Integer n)
-    | Node(_,"COMMAND",[c]) -> com_interp (evc,env,lfun,lmatch,goalopt) c
+    | Node(_,"COMMAND",[c]) ->
+      com_interp (evc,env,lfun,lmatch,goalopt,debug) c
     | Node(_,"CASTEDCOMMAND",[c]) ->
-      cast_com_interp (evc,env,lfun,lmatch,goalopt) c
+      cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) c
     | Node(_,"CASTEDOPENCOMMAND",[c]) ->
-      cast_opencom_interp (evc,env,lfun,lmatch,goalopt) c
+      cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) c
     | Node(_,"BINDINGS",astl) ->
-      VArg (Cbindings (List.map (bind_interp evc env lfun lmatch goalopt)
-        astl))
+      VArg (Cbindings (List.map (bind_interp
+        (evc,env,lfun,lmatch,goalopt,debug)) astl))
     | Node(_,"REDEXP",[Node(_,redname,args)]) ->
-      VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt)
+      VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug)
         (redname,args)))
     | Node(_,"CLAUSE",cl) ->
       VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp
-        (evc,env,lfun,lmatch,goalopt) ast))) cl))
-    | Node(_,"TACTIC",[ast]) -> VArg (Tac (tac_interp lfun lmatch ast))
+        (evc,env,lfun,lmatch,goalopt,debug) ast))) cl))
+    | Node(_,"TACTIC",[ast]) ->
+      VArg (Tac (tac_interp lfun lmatch debug ast))
 (*Remains to treat*)
     | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
       VArg ((Fixexp (id_of_string s,n,c)))
@@ -438,34 +479,45 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt) ast =
       VArg ((Cofixexp (id_of_string s,c)))
 (*End of Remains to treat*)
     | Node(_,"INTROPATTERN", [ast]) ->
-      VArg ((Intropattern (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)
-        ast)))
+      VArg ((Intropattern (cvt_intro_pattern
+        (evc,env,lfun,lmatch,goalopt,debug) ast)))
     | Node(_,"LETPATTERNS",astl) ->
       VArg (Letpatterns (List.fold_left (cvt_letpattern
-        (evc,env,lfun,lmatch,goalopt)) (None,[]) astl))
+        (evc,env,lfun,lmatch,goalopt,debug)) (None,[]) astl))
     | Node(loc,s,l) ->
       (try
-         ((look_for_interp s) (evc,env,lfun,lmatch,goalopt) ast)
+         ((look_for_interp s) (evc,env,lfun,lmatch,goalopt,debug) ast)
        with
            Not_found ->
-             val_interp (evc,env,lfun,lmatch,goalopt)
+             val_interp (evc,env,lfun,lmatch,goalopt,debug)
                (Node(dummy_loc,"APPTACTIC",[ast])))
+
+    | Dynamic(_,t) -> 
+      env_update (evc,env,lfun,lmatch,goalopt,debug);
+      let f = (ocamlOut t) in
+      Obj.magic (val_interp (evc,env,lfun,lmatch,goalopt,debug) (f ()))
     | _ ->
       anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR
-        "Unrecognizable ast: "; print_ast ast>])
+        "Unrecognizable ast: "; print_ast ast>]) in
+  if debug = DebugOn then
+    match debug_prompt goalopt ast with
+    | Exit -> VTactic tclIDTAC
+    | v -> value_interp v
+  else
+    value_interp debug
 
 (* Interprets an application node *)
-and app_interp evc env lfun lmatch goalopt fv largs ast =
+and app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast =
   match fv with
     | VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f)
     | VFun(olfun,var,body) ->
       let (newlfun,lvar,lval)=head_with_value (var,largs) in
       if lvar=[] then
         if lval=[] then
-          val_interp (evc,env,(olfun@newlfun),lmatch,goalopt) body
+          val_interp (evc,env,(olfun@newlfun),lmatch,goalopt,debug) body
         else
-          app_interp evc env lfun lmatch goalopt (val_interp (evc,env,
-            (olfun@newlfun),lmatch,goalopt) body) lval ast
+          app_interp (evc,env,lfun,lmatch,goalopt,debug) (val_interp (evc,env,
+            (olfun@newlfun),lmatch,goalopt,debug) body) lval ast
       else
         VFun(olfun@newlfun,lvar,body)
     | _ ->
@@ -473,7 +525,7 @@ and app_interp evc env lfun lmatch goalopt fv largs ast =
         "Illegal application: "; print_ast ast>])
 
 (* Interprets recursive expressions *)
-and rec_interp evc env lfun lmatch goalopt ast = function
+and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
   | [Node(_,"RECCLAUSE",_)] as l ->
      let (name,var,body) = List.hd (read_rec_clauses l)
      and ve = ref VVoid in
@@ -491,24 +543,24 @@ and rec_interp evc env lfun lmatch goalopt ast = function
       var,body))) lrc in
     begin
       List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
-      val_interp (evc,env,(lfun@lve),lmatch,goalopt) u
+      val_interp (evc,env,(lfun@lve),lmatch,goalopt,debug) u
     end
   | _ ->
     anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR
       "Rec not well formed: "; print_ast ast>])
 
 (* Interprets the clauses of a let *)
-and let_interp evc env lfun lmatch goalopt ast = function
+and let_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function
   | [] -> []
   | Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
-    (id,val_interp (evc,env,lfun,lmatch,goalopt) t)::(let_interp evc env lfun
-       lmatch goalopt ast tl)
+    (id,val_interp (evc,env,lfun,lmatch,goalopt,debug) t)::
+      (let_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl)
   | _ ->
     anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR
       "Let not well formed: "; print_ast ast>])
 
 (* Interprets the Match Context expressions *)
-and match_context_interp evc env lfun lmatch goalopt ast lmr =
+and match_context_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
   let goal =
     (match goalopt with
     | None ->
@@ -521,10 +573,11 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr =
       let (lgoal,ctxt) = sub_match nocc c csr in
       let lctxt = give_context ctxt id in
       if mhyps = [] then
-        eval_with_fail (val_interp (evc,env,lctxt@lfun,lgoal@lmatch,Some goal))
-          mt goal
+        eval_with_fail (val_interp
+          (evc,env,lctxt@lfun,lgoal@lmatch,Some goal,debug)) mt goal
       else
-        apply_hyps_context evc env (lctxt@lfun) lmatch goal mt lgoal mhyps hyps
+        apply_hyps_context evc env (lctxt@lfun) lmatch goal debug mt lgoal
+          mhyps hyps
     with
     | (FailError _) as e -> raise e
     | NextOccurrence _ -> raise No_match
@@ -533,26 +586,33 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr =
         hyps in
   let rec apply_match_context evc env lfun lmatch goal = function
     | (All t)::tl ->
-      (try eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal)) t goal
-       with No_match -> apply_match_context evc env lfun lmatch goal tl)
+      (try
+         eval_with_fail (val_interp (evc,env,lfun,lmatch,Some goal,debug)) t
+           goal
+       with No_match | _ -> apply_match_context evc env lfun lmatch goal tl)
     | (Pat (mhyps,mgoal,mt))::tl ->
-      let hyps = make_hyps (pf_hyps goal)
+      let hyps = make_hyps (List.rev (pf_hyps goal))
       and concl = pf_concl goal in
       (match mgoal with
       |	Term mg ->
         (try
            (let lgoal = apply_matching mg concl in
+            begin
+            db_matched_concl debug env concl;
             if mhyps = [] then
-              eval_with_fail (val_interp (evc,env,lfun,lgoal@lmatch,Some goal))
-                mt goal
+              eval_with_fail (val_interp
+                (evc,env,lfun,lgoal@lmatch,Some goal,debug)) mt goal
             else
-              apply_hyps_context evc env lfun lmatch goal mt lgoal mhyps hyps)
-         with | No_match -> apply_match_context evc env lfun lmatch goal tl)
+              apply_hyps_context evc env lfun lmatch goal debug mt lgoal mhyps
+                hyps
+            end)
+         with | No_match | _ ->
+           apply_match_context evc env lfun lmatch goal tl)
       |	Subterm (id,mg) ->
         (try
           apply_goal_sub evc env lfun lmatch goal 0 (id,mg) concl mt mhyps hyps
          with
-        | No_match -> apply_match_context evc env lfun lmatch goal tl))
+        | No_match | _ -> apply_match_context evc env lfun lmatch goal tl))
     | _ ->
       errorlabstrm "Tacinterp.apply_match_context" [<'sTR
         "No matching clauses for Match Context">] in
@@ -560,24 +620,26 @@ and match_context_interp evc env lfun lmatch goalopt ast lmr =
     (constr_list goalopt lfun) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps
-  hyps =
+and apply_hyps_context evc env lfun_glob lmatch_glob goal debug mt lgmatch
+  mhyps hyps =
   let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun
     lmatch mhyps lhyps_mhyp lhyps_rest noccopt =
     match mhyps with
       | hd::tl ->
         let (lid,lc,lm,newlhyps,hyp_match,noccopt) =
           apply_one_mhyp_context lmatch hd lhyps_mhyp noccopt in
+        begin
+        db_matched_hyp debug env hyp_match;
         (try
         if tl = [] then
             eval_with_fail (val_interp (evc,env,(lfun@lid@lc@lfun_glob),
-              (lmatch@lm@lmatch_glob),Some goal)) mt goal
+              (lmatch@lm@lmatch_glob),Some goal,debug)) mt goal
         else
           let nextlhyps =
             List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) []
               lhyps_rest in
           apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt
-            (lfun@lid@lc) (lmatch@lm) tl  nextlhyps nextlhyps None
+            (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
          with
         | (FailError _) as e -> raise e
         | _ ->
@@ -589,6 +651,7 @@ and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps
             apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun
               lmatch mhyps (hyp_match::newlhyps) lhyps_rest (Some (nocc +
               1))))
+        end
       |	[] ->
         anomalylabstrm "apply_hyps_context_rec" [<'sTR
           "Empty list should not occur" >] in
@@ -596,90 +659,101 @@ and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps
     hyps hyps None
 
 (* Interprets the Match expressions *)
-and match_interp evc env lfun lmatch goalopt ast lmr =
-  let rec apply_sub_match evc env lfun lmatch goalopt nocc (id,c) csr mt =
+and match_interp (evc,env,lfun,lmatch,goalopt,debug) ast lmr =
+  let rec apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) nocc (id,c) csr
+    mt =
     match goalopt with
     | None ->
       (try 
         let (lm,ctxt) = sub_match nocc c csr in
         let lctxt = give_context ctxt id in
-        val_interp (evc,env,lctxt@lfun,lm@lmatch,goalopt) mt
+        val_interp (evc,env,lctxt@lfun,lm@lmatch,goalopt,debug) mt
        with | NextOccurrence _ -> raise No_match)
     | Some g ->
       (try
         let (lm,ctxt) = sub_match nocc c csr in
         let lctxt = give_context ctxt id in
-        eval_with_fail (val_interp (evc,env,lctxt@lfun,lm@lmatch,goalopt)) mt g
+        eval_with_fail (val_interp
+          (evc,env,lctxt@lfun,lm@lmatch,goalopt,debug)) mt g
        with
        | NextOccurrence n -> raise No_match
        | (FailError _) as e -> raise e
        | _ ->
-         apply_sub_match evc env lfun lmatch goalopt (nocc + 1) (id,c) csr mt)
+         apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) (nocc + 1) (id,c)
+           csr mt)
   in
-  let rec apply_match evc env lfun lmatch goalopt csr = function
-    | (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t
+  let rec apply_match (evc,env,lfun,lmatch,goalopt,debug) csr = function
+    | (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt,debug) t
     | (Pat ([],mp,mt))::tl ->
       (match mp with
       |	Term c ->
         (try
-           val_interp (evc,env,lfun,(apply_matching c csr)@lmatch,goalopt) mt
-         with | No_match -> apply_match evc env lfun lmatch goalopt csr tl)
+           val_interp
+             (evc,env,lfun,(apply_matching c csr)@lmatch,goalopt,debug) mt
+         with | No_match ->
+           apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl)
       |	Subterm (id,c) ->
-        (try apply_sub_match evc env lfun lmatch goalopt 0 (id,c) csr mt
-         with | No_match -> apply_match evc env lfun lmatch goalopt csr tl))
+        (try
+           apply_sub_match (evc,env,lfun,lmatch,goalopt,debug) 0 (id,c) csr mt
+         with | No_match ->
+           apply_match (evc,env,lfun,lmatch,goalopt,debug) csr tl))
     | _ ->
       errorlabstrm "Tacinterp.apply_match" [<'sTR
         "No matching clauses for Match">] in
-  let csr = constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-    (List.hd lmr)))
+  let csr =
+    constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug)
+      (List.hd lmr)))
   and ilr = read_match_rule evc env (constr_list goalopt lfun) (List.tl lmr) in
-  apply_match evc env lfun lmatch goalopt csr ilr
+  apply_match (evc,env,lfun,lmatch,goalopt,debug) csr ilr
 
 (* Interprets tactic expressions *)
-and tac_interp lfun lmatch ast g =
+and tac_interp lfun lmatch debug ast g =
   let evc = project g
   and env = pf_env g in
-    match (val_interp (evc,env,lfun,lmatch,(Some g)) ast) with
+    match (val_interp (evc,env,lfun,lmatch,(Some g),debug) ast) with
       | VTactic tac -> (tac g)
       | VFTactic (largs,f) -> (f largs g) 
       | VRTactic res -> res
       | _ ->
-        errorlabstrm "Tacinterp.interp_rec" [<'sTR
+        errorlabstrm "Tacinterp.tac_interp" [<'sTR
           "Interpretation gives a non-tactic value">]
 
 (* Interprets a primitive tactic *)
 and interp_atomic loc opn args = vernac_tactic(opn,args)
 
 (* Interprets sequences of tactics *)
-and interp_semi_list acc lfun lmatch = function
+and interp_semi_list acc lfun lmatch debug = function
   | (Node(_,"TACLIST",seq))::l ->
-    interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch) seq))
-      lfun lmatch l
+    interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch debug)
+      seq)) lfun lmatch debug l
   | t::l ->
-    interp_semi_list (tclTHEN acc (tac_interp lfun lmatch t)) lfun lmatch l
+    interp_semi_list (tclTHEN acc (tac_interp lfun lmatch debug t)) lfun lmatch
+      debug l
   | [] -> acc
 
 (* Interprets bindings for tactics *)
-and bind_interp evc env lfun lmatch goalopt = function
+and bind_interp (evc,env,lfun,lmatch,goalopt,debug) = function
   | Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) ->
-    (NoDep n,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-       (Node(loc,"COMMAND",[c])))))
+    (NoDep n,constr_of_Constr (unvarg (val_interp
+      (evc,env,lfun,lmatch,goalopt,debug) (Node(loc,"COMMAND",[c])))))
   | Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> 
-    (Dep (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-       (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp
-       (evc,env,lfun,lmatch,goalopt) (Node(loc1,"COMMAND",[c])))))
+    (Dep (id_of_Identifier (unvarg (val_interp
+      (evc,env,lfun,lmatch,goalopt,debug)
+      (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp
+      (evc,env,lfun,lmatch,goalopt,debug) (Node(loc1,"COMMAND",[c])))))
   | Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) ->
-    (Com,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-       (Node(loc,"COMMAND",[c])))))
+    (Com,constr_of_Constr (unvarg
+      (val_interp (evc,env,lfun,lmatch,goalopt,debug)
+      (Node(loc,"COMMAND",[c])))))
   | x ->
     errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding";
       print_ast x>]
 
 (* Interprets a COMMAND expression (in case of failure, returns Command) *)
-and com_interp (evc,env,lfun,lmatch,goalopt) = function
+and com_interp (evc,env,lfun,lmatch,goalopt,debug) = function
   | Node(_,"EVAL",[c;rtc]) ->
-    let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-      rtc)) in
+    let redexp = unredexp (unvarg (val_interp
+      (evc,env,lfun,lmatch,goalopt,debug) rtc)) in
     VArg (Constr ((reduction_of_redexp redexp) env evc
 		    (interp_constr_gen evc env (constr_list goalopt lfun)
 		       lmatch c None)))
@@ -694,19 +768,18 @@ and com_interp (evc,env,lfun,lmatch,goalopt) = function
       errorlabstrm "com_interp" [<'sTR "Unbound context identifier";
         print_ast ast>])
   | c ->
-(*    try*)
       VArg (Constr
 	      (interp_constr_gen evc env (constr_list goalopt lfun) lmatch
 		 c None))
-(*    with e when Logic.catchable_exception e -> VArg (Command c)*)
 
 (* Interprets a CASTEDCOMMAND expression *)
-and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with
+and cast_com_interp (evc,env,lfun,lmatch,goalopt,debug) com =
+  match goalopt with
   | Some gl ->
     (match com with
     | Node(_,"EVAL",[c;rtc]) ->
-      let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-        rtc)) in
+      let redexp = unredexp (unvarg (val_interp
+        (evc,env,lfun,lmatch,goalopt,debug) rtc)) in
       VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen
         evc env (constr_list goalopt lfun) lmatch c (Some (pf_concl gl)))))
     | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast ->
@@ -724,20 +797,19 @@ and cast_com_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with
         errorlabstrm "cast_com_interp" [<'sTR "Unbound context identifier";
           print_ast ast>])
     | c ->
-(*      try*)
         VArg (Constr (interp_constr_gen evc env (constr_list goalopt lfun)
-          lmatch c (Some (pf_concl gl))))
-(*      with e when Logic.catchable_exception e -> VArg (Command c)*) )
+          lmatch c (Some (pf_concl gl)))))
   | None ->
     errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
 
 (* Interprets a CASTEDOPENCOMMAND expression *)
-and cast_opencom_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with
+and cast_opencom_interp (evc,env,lfun,lmatch,goalopt,debug) com =
+  match goalopt with
   | Some gl ->
     (match com with
     | Node(_,"EVAL",[c;rtc]) ->
-      let redexp = unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-        rtc)) in
+      let redexp = unredexp (unvarg (val_interp
+        (evc,env,lfun,lmatch,goalopt,debug) rtc)) in
       VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr_gen
         evc env (constr_list goalopt lfun) lmatch c (Some (pf_concl gl)))))
     | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast ->
@@ -755,37 +827,36 @@ and cast_opencom_interp (evc,env,lfun,lmatch,goalopt) com = match goalopt with
         errorlabstrm "cast_opencom_interp" [<'sTR "Unbound context identifier";
           print_ast ast>])
     | c ->
-(*      try*)
         VArg
 	  (OpenConstr (interp_openconstr_gen evc env (constr_list goalopt lfun)
-			 lmatch c (Some (pf_concl gl))))
-(*      with e when Logic.catchable_exception e -> VArg (Command c)*) )
+			 lmatch c (Some (pf_concl gl)))))
   | None ->
     errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
 
-and cvt_pattern (evc,env,lfun,lmatch,goalopt) = function
+and cvt_pattern (evc,env,lfun,lmatch,goalopt,debug) = function
   | Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) ->
       let occs = List.map num_of_ast nums
       and csr = constr_of_Constr (unvarg (val_interp
-        (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[com])))) in
+        (evc,env,lfun,lmatch,goalopt,debug) (Node(loc,"COMMAND",[com])))) in
       let jdt = Typing.unsafe_machine env evc csr in
       (occs, jdt.Environ.uj_val, body_of_type jdt.Environ.uj_type)
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
 
-and cvt_unfold (evc,env,lfun,lmatch,goalopt) = function
+and cvt_unfold (evc,env,lfun,lmatch,goalopt,debug) = function
   | Node(_,"UNFOLD", com::nums) ->
     (List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp
-       (evc,env,lfun,lmatch,goalopt) com))))
+       (evc,env,lfun,lmatch,goalopt,debug) com))))
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold")
 
 (* Interprets the arguments of Fold *)
-and cvt_fold (evc,env,lfun,lmatch,goalopt) = function
+and cvt_fold (evc,env,lfun,lmatch,goalopt,debug) = function
   | Node(_,"COMMAND",[c]) as ast ->
-    constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast))
+    constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt,debug)
+      ast))
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold")
 
 (* Interprets the reduction flags *)
-and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf =
+and flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf =
   let rec add_flag red = function
     | [] -> red
     | Node(_,"Beta",[])::lf -> add_flag (red_add red BETA) lf
@@ -794,12 +865,12 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf =
 	   | Node(loc,"Unf",l)::lf ->
                let idl=
 		 List.map (fun v -> glob_nvar (id_of_Identifier (unvarg
-		   (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l
+		   (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l
 	       in add_flag (red_add red (CONST idl)) lf
 	   | Node(loc,"UnfBut",l)::lf ->
                let idl=
 		 List.map (fun v -> glob_nvar (id_of_Identifier (unvarg
-                   (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l
+                   (val_interp (evc,env,lfun,lmatch,goalopt,debug) v)))) l
                in add_flag (red_add red (CONSTBUT idl)) lf
 	   | _ -> add_flag (red_add red DELTA) lf)
     | Node(_,"Iota",[])::lf -> add_flag (red_add red IOTA) lf
@@ -812,40 +883,47 @@ and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf =
   add_flag no_red lf;
 
 (* Interprets a reduction expression *)
-and redexp_of_ast (evc,env,lfun,lmatch,goalopt) = function
+and redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) = function
   | ("Red", []) -> Red false
   | ("Hnf", []) -> Hnf
   | ("Simpl", []) -> Simpl
   | ("Unfold", ul) ->
-    Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt)) ul)
-  | ("Fold", cl) -> Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt)) cl)
-  | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf)
-  | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf)
+    Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt,debug)) ul)
+  | ("Fold", cl) ->
+    Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt,debug)) cl)
+  | ("Cbv",lf) ->
+    Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf)
+  | ("Lazy",lf) ->
+    Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt,debug) lf)
   | ("Pattern",lp) ->
-    Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt)) lp)
+    Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt,debug)) lp)
   | (s,_) -> invalid_arg ("malformed reduction-expression: "^s)
 
 (* Interprets the patterns of Intro *)
-and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt) = function
+and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug) = function
   | Node(_,"IDENTIFIER", [Nvar(loc,s)]) ->
-    IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-      (Nvar (loc,s)))))
+    IdPat (id_of_Identifier (unvarg (val_interp
+      (evc,env,lfun,lmatch,goalopt,debug) (Nvar (loc,s)))))
   | Node(_,"DISJPATTERN", l) ->
-    DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l)
+    DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug))
+      l)
   | Node(_,"CONJPATTERN", l) ->
-    ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l)
+    ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug))
+      l)
   | Node(_,"LISTPATTERN", l) ->
-    ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l)
+    ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt,debug))
+      l)
   | x ->
     errorlabstrm "cvt_intro_pattern"
       [<'sTR "Not the expected form for an introduction pattern!"; print_ast
         x>]
 
 (* Interprets a pattern of Let *)
-and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l) = function
+and cvt_letpattern (evc,env,lfun,lmatch,goalopt,debug) (o,l) = function
   | Node(_,"HYPPATTERN", Nvar(loc,s)::nums) ->
-    (o,(id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
-       (Nvar (loc,s)))),List.map num_of_ast nums)::l)
+    (o,(id_of_Identifier (unvarg (val_interp
+      (evc,env,lfun,lmatch,goalopt,debug)
+      (Nvar (loc,s)))),List.map num_of_ast nums)::l)
   | Node(_,"CCLPATTERN", nums) ->
     if o <> None then
       error "\"Goal\" occurs twice"
@@ -857,7 +935,7 @@ and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l) = function
 let interp_tacarg sign ast = unvarg (val_interp sign ast)
 
 (* Initial call for interpretation *)
-let interp = tac_interp [] []
+let interp = fun ast -> tac_interp [] [] !debug ast
 
 let is_just_undef_macro ast =
   match ast with
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 746c89f08..ee5d67966 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
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
new file mode 100644
index 000000000..d9c5d528a
--- /dev/null
+++ b/proofs/tactic_debug.ml
@@ -0,0 +1,47 @@
+open Ast
+open Pp
+open Printer
+
+(* 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 goal if it exists *)
+let db_pr_goal = function
+  | None -> mSGNL [< 'sTR "No goal" >]
+  | Some g ->
+    mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >]
+
+(* 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----" >];
+  let rec prompt () =
+    mSG [<'fNL; 'sTR "TcDebug> " >];
+    flush stdout;
+    let inst = read_line () in
+    mSGNL [<>];
+    match inst with
+    | ""  -> DebugOn
+    | "s" -> DebugOff
+    | "x" -> Exit
+    | _   -> prompt () in
+  prompt ()
+
+(* Prints a matched hypothesis *)
+let db_matched_hyp debug env (id,c) =
+  if debug = DebugOn then
+    mSGNL [< 'sTR "Matched hypothesis --> "; 'sTR (id^": ");
+             prterm_env env c >]
+
+(* Prints the matched conclusion *)
+let db_matched_concl debug env c =
+  if debug = DebugOn then
+    mSGNL [< 'sTR "Matched goal --> "; prterm_env env c >]
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
new file mode 100644
index 000000000..26ab1a947
--- /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