Debugger plus informatif

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

8 files changed, 333 insertions, 162 deletions

diff --git a/.depend b/.depend
index c741efbcd3..c3a3695dcf 100644
--- a/.depend
+++ b/.depend
@@ -122,7 +122,7 @@ parsing/ppconstr.cmi: parsing/coqast.cmi kernel/environ.cmi \
     lib/pp.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo kernel/term.cmi \
     interp/topconstr.cmi lib/util.cmi 
 parsing/pptactic.cmi: parsing/egrammar.cmi interp/genarg.cmi lib/pp.cmi \
-    proofs/proof_type.cmi proofs/tacexpr.cmo 
+    pretyping/pretyping.cmi proofs/proof_type.cmi proofs/tacexpr.cmo 
 parsing/prettyp.cmi: pretyping/classops.cmi kernel/environ.cmi \
     library/impargs.cmi library/lib.cmi library/libnames.cmi kernel/names.cmi \
     library/nametab.cmi lib/pp.cmi pretyping/reductionops.cmi \
@@ -220,7 +220,8 @@ proofs/tacmach.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
     kernel/sign.cmi proofs/tacexpr.cmo pretyping/tacred.cmi kernel/term.cmi \
     interp/topconstr.cmi 
 proofs/tactic_debug.cmi: kernel/environ.cmi kernel/names.cmi \
-    proofs/proof_type.cmi proofs/tacexpr.cmo kernel/term.cmi 
+    pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacexpr.cmo \
+    kernel/term.cmi 
 tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/environ.cmi \
     pretyping/evd.cmi library/libnames.cmi kernel/names.cmi \
     pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \
@@ -1422,16 +1423,14 @@ proofs/tacmach.cmx: interp/constrintern.cmx library/declare.cmx \
     proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx \
     pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \
     pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi 
-proofs/tactic_debug.cmo: parsing/ast.cmi library/libnames.cmi \
-    proofs/logic.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \
-    parsing/pptactic.cmi pretyping/pretype_errors.cmi parsing/printer.cmi \
-    proofs/proof_trees.cmi proofs/tacmach.cmi kernel/type_errors.cmi \
-    lib/util.cmi proofs/tactic_debug.cmi 
-proofs/tactic_debug.cmx: parsing/ast.cmx library/libnames.cmx \
-    proofs/logic.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \
-    parsing/pptactic.cmx pretyping/pretype_errors.cmx parsing/printer.cmx \
-    proofs/proof_trees.cmx proofs/tacmach.cmx kernel/type_errors.cmx \
-    lib/util.cmx proofs/tactic_debug.cmi 
+proofs/tactic_debug.cmo: parsing/ast.cmi interp/constrextern.cmi \
+    kernel/names.cmi lib/pp.cmi parsing/pptactic.cmi parsing/printer.cmi \
+    proofs/proof_trees.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \
+    pretyping/termops.cmi proofs/tactic_debug.cmi 
+proofs/tactic_debug.cmx: parsing/ast.cmx interp/constrextern.cmx \
+    kernel/names.cmx lib/pp.cmx parsing/pptactic.cmx parsing/printer.cmx \
+    proofs/proof_trees.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \
+    pretyping/termops.cmx proofs/tactic_debug.cmi 
 scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi 
 scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx 
 scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo 
@@ -1833,13 +1832,13 @@ tools/gallina.cmx: tools/gallina_lexer.cmx
 toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
     kernel/indtypes.cmi parsing/lexer.cmi library/libnames.cmi \
     proofs/logic.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    pretyping/pretype_errors.cmi proofs/refiner.cmi kernel/type_errors.cmi \
-    kernel/univ.cmi lib/util.cmi toplevel/cerrors.cmi 
+    pretyping/pretype_errors.cmi proofs/refiner.cmi proofs/tactic_debug.cmi \
+    kernel/type_errors.cmi kernel/univ.cmi lib/util.cmi toplevel/cerrors.cmi 
 toplevel/cerrors.cmx: parsing/ast.cmx pretyping/cases.cmx toplevel/himsg.cmx \
     kernel/indtypes.cmx parsing/lexer.cmx library/libnames.cmx \
     proofs/logic.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    pretyping/pretype_errors.cmx proofs/refiner.cmx kernel/type_errors.cmx \
-    kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi 
+    pretyping/pretype_errors.cmx proofs/refiner.cmx proofs/tactic_debug.cmx \
+    kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx toplevel/cerrors.cmi 
 toplevel/class.cmo: pretyping/classops.cmi library/decl_kinds.cmo \
     kernel/declarations.cmi library/declare.cmi kernel/entries.cmi \
     kernel/environ.cmi pretyping/evd.cmi library/global.cmi \
diff --git a/Makefile b/Makefile
index f12d074d33..b0aaedbc86 100644
--- a/Makefile
+++ b/Makefile
@@ -232,11 +232,11 @@ PARSERREQUIRES=\
   parsing/ppconstr.cmo parsing/printer.cmo parsing/pptactic.cmo $(TRANSLATE) \
   pretyping/typing.cmo proofs/proof_trees.cmo \
   proofs/logic.cmo proofs/refiner.cmo proofs/evar_refiner.cmo \
-  proofs/tacmach.cmo toplevel/himsg.cmo parsing/g_natsyntax.cmo \
-  parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo toplevel/class.cmo \
-  toplevel/recordobj.cmo toplevel/cerrors.cmo parsing/g_vernac.cmo \
-  parsing/g_proofs.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo \
-  parsing/g_constr.cmo parsing/g_cases.cmo proofs/tactic_debug.cmo \
+  proofs/tacmach.cmo proofs/tactic_debug.cmo toplevel/himsg.cmo \
+  parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \
+  toplevel/class.cmo toplevel/recordobj.cmo toplevel/cerrors.cmo \
+  parsing/g_vernac.cmo parsing/g_proofs.cmo parsing/g_tactic.cmo \
+  parsing/g_ltac.cmo parsing/g_constr.cmo parsing/g_cases.cmo \
   proofs/pfedit.cmo proofs/clenv.cmo tactics/wcclausenv.cmo \
   tactics/tacticals.cmo tactics/hipattern.cmo tactics/tactics.cmo \
   tactics/hiddentac.cmo tactics/dn.cmo tactics/termdn.cmo \
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index a3963571c9..ca16c21e53 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -11,6 +11,7 @@
 open Pp
 open Genarg
 open Tacexpr
+open Pretyping
 open Proof_type
 
 val declare_extra_genarg_pprule : 
@@ -25,6 +26,8 @@ val declare_extra_tactic_pprule :
       string * Egrammar.grammar_tactic_production list)
       -> unit 
 
+val pr_match_pattern : Tacexpr.pattern_expr match_pattern -> std_ppcmds
+
 val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) ->
   (pattern_expr,raw_tactic_expr) match_rule -> std_ppcmds
 
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 316aa0ee53..592f3a2eab 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -5,10 +5,14 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+
 open Ast
+open Constrextern
 open Pp
 open Pptactic
 open Printer
+open Tacexpr
+open Termops
 
 (* 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
@@ -16,78 +20,158 @@ open Printer
 
 (* Debug information *)
 type debug_info =
-  | DebugOn of int
+  | DebugOn
   | DebugOff
+  | Run of int
 
-(* 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 goal *)
+let db_pr_goal 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 raised exceptions *)
-let rec db_print_error = function
-  | Type_errors.TypeError(ctx,te) -> 
-      hov 0 (str "Type error:" ++ spc ())
-  | Pretype_errors.PretypeError(ctx,te) ->
-      hov 0 (str "Pretype error:" ++ spc ())
-  | Logic.RefinerError e -> 
-      hov 0 (str "Refiner error:" ++ spc ())
-  | Stdpp.Exc_located (loc,exc) ->
-      db_print_error exc
-  | Util.UserError(s,pps) -> 
-      hov 1 (str"Error: " ++ pps)
-  | Nametab.GlobalizationError q ->
-      hov 0 (str "Error: " ++ Libnames.pr_qualid q ++ str " not found")
-  | _ ->
-      hov 0 (str "Uncaught exception ")
+  msgnl (str "Commands: <Enter>=Continue" ++ fnl() ++
+         str "          h/?=Help" ++ fnl() ++
+         str "          r<num>=Run <num> times" ++ fnl() ++
+         str "          s=Skip" ++ fnl() ++
+         str "          x=Exit")
 
-(* Prints the state and waits for an instruction *)
-let debug_prompt level goalopt tac_ast f =
-  db_pr_goal goalopt;
-  msg (str "Going to execute:" ++ fnl () ++ (pr_raw_tactic 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 (" ++ int level ++ str ") > ");
+(* Prints the goal and the command to be executed *)
+let goal_com g tac_ast =
+  begin
+    db_pr_goal g;
+    msg (str "Going to execute:" ++ fnl () ++ (pr_raw_tactic tac_ast) ++
+         fnl ())
+  end
+
+(* Gives the number of a run command *)
+let run_com inst =
+  if (String.get inst 0)='r' then
+    let num = int_of_string (String.sub inst 1 ((String.length inst)-1)) in
+    if num>0 then num
+    else raise (Invalid_argument "run_com")
+  else
+    raise (Invalid_argument "run_com")
+
+(* Prints the run counter *)
+let run ini ctr =
+  if ini then msg (str "Executed expressions: 0" ++ fnl() ++ fnl())
+  else
+  begin
+    for i=1 to 2 do
+      print_char (Char.chr 8);print_char (Char.chr 13)
+    done;
+    msg (str "Executed expressions: " ++ int ctr ++ fnl() ++ fnl())
+  end
+
+(* Prints the prompt *)
+let rec prompt () =
+  begin
+    msg (fnl () ++ str "TcDebug > ");
     flush stdout;
     let inst = read_line () in
-(*    mSGNL (mt ());*)
     match inst with
-    | ""  -> DebugOn (level+1)
+    | ""  -> DebugOn
     | "s" -> DebugOff
-    | "x" -> raise Sys.Break
-    | "h" ->
+    | "x" -> print_char (Char.chr 8);raise Sys.Break
+    | "h"| "?" ->
       begin
         help ();
         prompt ()
       end
-    | _   -> prompt () in
-  let d = prompt () in
-  try f d
-  with e when e <> Sys.Break ->
-    ppnl (str "Level " ++ int level ++ str ": " ++ db_print_error e); 
-    raise e
+    | _ ->
+      (try let ctr=run_com inst in run true ctr;Run ctr
+       with Failure _ | Invalid_argument _ -> prompt ())
+  end
+
+(* Prints the whole state *)
+let state g tac_ast ctr =
+  begin
+    goal_com g tac_ast;
+    let debug = prompt () in
+    match debug with
+    | Run n -> ctr := 0;debug
+    | _ -> debug
+  end
+
+(* Prints the state and waits for an instruction *)
+let debug_prompt =
+  let ctr = ref 0 in
+  fun g debug tac_ast ->
+  match debug with
+  | Run n ->
+    if !ctr=n then state g tac_ast ctr
+    else (incr ctr;run false !ctr;debug)
+  | _ -> state g tac_ast ctr
 
 (* Prints a constr *)
 let db_constr debug env c =
   if debug <> DebugOff then
-    msgnl (str "Evaluated term --> " ++ prterm_env env c)
+    msgnl (str "Evaluated term: " ++ prterm_env env c)
+
+(* Prints the pattern rule *)
+let db_pattern_rule debug num r =
+  if debug = DebugOn then
+  begin
+    msgnl (str "Pattern rule " ++ int num ++ str ":");
+    msgnl (str "|" ++ spc () ++ pr_match_rule false pr_raw_tactic r)
+  end
+
+(* Prints the hypothesis pattern identifier if it exists *)
+let hyp_bound = function
+  | None -> " (unbound)"
+  | Some id -> " (bound to "^(Names.string_of_id id)^")"
 
 (* Prints a matched hypothesis *)
-let db_matched_hyp debug env (id,c) =
-  if debug <> DebugOff then
-    msgnl (str "Matched hypothesis --> " ++ str (Names.string_of_id id^": ") ++
-           prterm_env env c)
+let db_matched_hyp debug env (id,c) ido =
+  if debug = DebugOn then
+    msgnl (str "Hypothesis " ++
+           str ((Names.string_of_id id)^(hyp_bound ido)^
+                " has been matched: ") ++ prterm_env env c)
 
 (* Prints the matched conclusion *)
 let db_matched_concl debug env c =
-  if debug <> DebugOff then
-    msgnl (str "Matched goal --> " ++ prterm_env env c)
+  if debug = DebugOn then
+    msgnl (str "Conclusion has been matched: " ++ prterm_env env c)
+
+(* Prints a success message when the goal has been matched *)
+let db_mc_pattern_success debug =
+  if debug = DebugOn then
+    msgnl (str "The goal has been successfully matched!" ++ fnl() ++
+           str "Let us execute the right-hand side part..." ++ fnl())
+
+let pp_match_pattern env = function
+  | Term c -> Term (extern_pattern env (names_of_rel_context env) c)
+  | Subterm (o,c) ->
+    Subterm (o,(extern_pattern env (names_of_rel_context env) c))
+
+(* Prints a failure message for an hypothesis pattern *)
+let db_hyp_pattern_failure debug env hyp =
+  if debug = DebugOn then
+    msgnl (str ("The pattern hypothesis"^(hyp_bound (fst hyp))^
+                " cannot match: ") ++
+           pr_match_pattern (pp_match_pattern env (snd hyp)))
+
+(* Prints a matching failure message for a rule *)
+let db_matching_failure debug =
+  if debug = DebugOn then
+    msgnl (str "This rule has failed due to matching errors!" ++ fnl() ++
+           str "Let us try the next one...")
+
+(* Prints an evaluation failure message for a rule *)
+let db_eval_failure debug =
+  if debug = DebugOn then
+    msgnl (str "This rule has failed due to \"Fail\" tactic (level 0)!" ++
+           fnl() ++ str "Let us try the next one...")
+
+(* An exception handler *)
+let explain_logic_error = ref (fun e -> mt())
 
+(* Prints a logic failure message for a rule *)
+let db_logic_failure debug err =
+  if debug = DebugOn then
+  begin
+    msgnl (!explain_logic_error err);
+    msgnl (str "This rule has failed due to a logic error!" ++ fnl() ++
+           str "Let us try the next one...")
+  end
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 9b542c7848..8c5dc9d03c 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -8,8 +8,11 @@
 
 (*i $Id$ i*)
 
+open Environ
+open Pattern
 open Proof_type
 open Names
+open Tacexpr
 open Term
 
 (* This module intends to be a beginning of debugger for tactic expressions.
@@ -18,18 +21,43 @@ open Term
 
 (* Debug information *)
 type debug_info =
-  | DebugOn of int
+  | DebugOn
   | DebugOff
+  | Run of int
 
 (* Prints the state and waits *)
-val debug_prompt : int -> goal sigma option -> Tacexpr.raw_tactic_expr ->
-      (debug_info -> 'a) -> 'a
+val debug_prompt :
+  goal sigma -> debug_info -> Tacexpr.raw_tactic_expr -> debug_info
 
 (* Prints a constr *)
-val db_constr : debug_info -> Environ.env -> constr -> unit
+val db_constr : debug_info -> env -> constr -> unit
+
+(* Prints the pattern rule *)
+val db_pattern_rule :
+  debug_info -> int -> (pattern_expr,raw_tactic_expr) match_rule -> unit
 
 (* Prints a matched hypothesis *)
-val db_matched_hyp : debug_info -> Environ.env -> identifier * constr -> unit
+val db_matched_hyp :
+  debug_info -> env -> identifier * constr -> identifier option -> unit
 
 (* Prints the matched conclusion *)
-val db_matched_concl : debug_info -> Environ.env -> constr -> unit
+val db_matched_concl : debug_info -> env -> constr -> unit
+
+(* Prints a success message when the goal has been matched *)
+val db_mc_pattern_success : debug_info -> unit
+
+(* Prints a failure message for an hypothesis pattern *)
+val db_hyp_pattern_failure :
+  debug_info -> env -> identifier option * constr_pattern match_pattern -> unit
+
+(* Prints a matching failure message for a rule *)
+val db_matching_failure : debug_info -> unit
+
+(* Prints an evaluation failure message for a rule *)
+val db_eval_failure : debug_info -> unit
+
+(* An exception handler *)
+val explain_logic_error: (exn -> Pp.std_ppcmds) ref
+
+(* Prints a logic failure message for a rule *)
+val db_logic_failure : debug_info -> exn -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fdafe9a64d..3f9ad2fd79 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -253,13 +253,14 @@ let lookup_genarg_interp id =
   try Gmap.find id !extragenargtab
   with Not_found -> failwith ("No interpretation function found for entry "^id)
 
-
 (* Unboxes VRec *)
 let unrec = function
   | VRec v -> !v
   | a -> a
 
-(************* GLOBALIZE ************)
+(*****************)
+(* Globalization *)
+(*****************)
 
 (* We have identifier <| global_reference <| constr *)
 
@@ -369,7 +370,7 @@ let glob_induction_arg ist = function
   | ElimOnAnonHyp n as x -> x
   | ElimOnIdent (_loc,id) as x -> ElimOnIdent (loc,id)
 
-(* Globalize a reduction expression *)
+(* Globalizes a reduction expression *)
 let glob_evaluable_or_metanum ist = function
   | AN qid -> AN (glob_reference ist qid)
   | MetaNum (_loc,n) -> MetaNum (loc,glob_metanum ist loc n)
@@ -457,7 +458,8 @@ let extract_let_names lrc =
 (* Globalizes tactics *)
 let rec glob_atomic lf (_,_,_,_ as ist) = function
   (* Basic tactics *)
-  | TacIntroPattern l -> TacIntroPattern (List.map (glob_intro_pattern lf ist) l)
+  | TacIntroPattern l ->
+      TacIntroPattern (List.map (glob_intro_pattern lf ist) l)
   | TacIntrosUntil hyp -> TacIntrosUntil (glob_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
       TacIntroMove (option_app (glob_ident lf ist) ido,
@@ -493,7 +495,8 @@ let rec glob_atomic lf (_,_,_,_ as ist) = function
   | TacTrivial l -> TacTrivial l
   | TacAuto (n,l) -> TacAuto (n,l)
   | TacAutoTDB n -> TacAutoTDB n
-  | TacDestructHyp (b,(_loc,_ as id)) -> TacDestructHyp(b,(loc,glob_hyp ist id))
+  | TacDestructHyp (b,(_loc,_ as id)) ->
+      TacDestructHyp(b,(loc,glob_hyp ist id))
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
   | TacDAuto (n,p) -> TacDAuto (n,p)
@@ -524,7 +527,8 @@ let rec glob_atomic lf (_,_,_,_ as ist) = function
   (* Context management *)
   | TacClear l -> TacClear (List.map (glob_hyp_or_metanum ist) l)
   | TacClearBody l -> TacClearBody (List.map (glob_hyp_or_metanum ist) l)
-  | TacMove (dep,id1,id2) -> TacMove (dep,glob_lochyp ist id1,glob_lochyp ist id2)
+  | TacMove (dep,id1,id2) ->
+    TacMove (dep,glob_lochyp ist id1,glob_lochyp ist id2)
   | TacRename (id1,id2) -> TacRename (glob_lochyp ist id1, glob_lochyp ist id2)
 
   (* Constructors *)
@@ -568,11 +572,13 @@ and glob_tactic_seq (lfun,lmeta,sigma,env as ist) = function
       let lrc = List.map (fun (n,b) -> (n,glob_tactic_fun ist b)) lrc in
       lfun, TacLetRecIn (lrc,glob_tactic ist u)
   | TacLetIn (l,u) ->
-      let l = List.map (fun (n,c,b) -> (n,option_app (glob_constr_may_eval ist) c,glob_tacarg !strict_check ist b)) l in
+      let l = List.map (fun (n,c,b) -> (n,option_app (glob_constr_may_eval ist)
+              c,glob_tacarg !strict_check ist b)) l in
       let ist' = ((extract_let_names l)@lfun,lmeta,sigma,env) in
       lfun, TacLetIn (l,glob_tactic ist' u)
   | TacLetCut l ->
-      let f (n,c,t) = (n,glob_constr_may_eval ist c,glob_tacarg !strict_check ist t) in
+      let f (n,c,t) = (n,glob_constr_may_eval ist c,glob_tacarg !strict_check
+                      ist t) in
       lfun, TacLetCut (List.map f l)
   | TacMatchContext (lr,lmr) ->
       lfun, TacMatchContext(lr, glob_match_rule ist lmr)
@@ -657,7 +663,8 @@ and glob_genarg ist x =
   | ConstrArgType ->
       in_gen rawwit_constr (glob_constr ist (out_gen rawwit_constr x))
   | ConstrMayEvalArgType ->
-      in_gen rawwit_constr_may_eval (glob_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
+      in_gen rawwit_constr_may_eval (glob_constr_may_eval ist
+      (out_gen rawwit_constr_may_eval x))
   | QuantHypArgType ->
       in_gen rawwit_quant_hyp
         (glob_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
@@ -677,8 +684,7 @@ and glob_genarg ist x =
   | PairArgType _ -> app_pair (glob_genarg ist) (glob_genarg ist) x
   | ExtraArgType s -> x
 
-
-(************* END GLOBALIZE ************)
+(**** End Globalization ****)
 
 (* Associates variables with values and gives the remaining variables and
    values *)
@@ -733,9 +739,10 @@ let rec read_match_rule evc env lfun = function
 (* For Match Context and Match *)
 exception No_match
 exception Not_coherent_metas
+exception Eval_fail
 
 let is_match_catchable = function
-  | No_match | FailError _ -> true
+  | No_match | Eval_fail | FailError _ -> true
   | e -> Logic.catchable_exception e
 
 (* Verifies if the matched list is coherent with respect to lcm *)
@@ -755,14 +762,23 @@ let apply_matching pat csr =
      PatternMatchingFailure -> raise No_match
 
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
-let apply_one_mhyp_context gl lmatch mhyp lhyps noccopt =
+let apply_one_mhyp_context ist env gl lmatch mhyp lhyps noccopt =
   let get_pattern = function
     | Hyp (_,pat) -> pat
     | NoHypId pat -> pat
   and get_id_couple id = function
+    | Hyp((_,idpat),_) -> [idpat,VIdentifier id]
+    | NoHypId _ -> [] 
+  and get_info_pattern = function
+    | Hyp((_,idpat),pat) -> (Some idpat,pat)
+    | NoHypId pat -> (None,pat) in
+
+(*=======
     | Hyp((_,idpat),_) -> [idpat,VConstr (mkVar id)]
     | NoHypId _ -> [] in
-  let rec apply_one_mhyp_context_rec mhyp lhyps_acc nocc = function
+>>>>>>> 1.28*)
+
+  let rec apply_one_mhyp_context_rec ist env mhyp lhyps_acc nocc = function
     | (id,hyp)::tl ->
       (match (get_pattern mhyp) with
       | Term t ->
@@ -771,7 +787,7 @@ let apply_one_mhyp_context gl lmatch mhyp lhyps noccopt =
             verify_metas_coherence gl lmatch (Pattern.matches t hyp) in
           (get_id_couple id mhyp,[],lmeta,tl,(id,hyp),None)
          with | PatternMatchingFailure | Not_coherent_metas ->
-          apply_one_mhyp_context_rec mhyp (lhyps_acc@[id,hyp]) 0 tl)
+          apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl)
       | Subterm (ic,t) ->
         (try
           let (lm,ctxt) = sub_match nocc t hyp in
@@ -780,15 +796,37 @@ let apply_one_mhyp_context gl lmatch mhyp lhyps noccopt =
             ic,lmeta,tl,(id,hyp),Some nocc)
          with
         | NextOccurrence _ ->
-          apply_one_mhyp_context_rec mhyp (lhyps_acc@[id,hyp]) 0 tl
+          apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl
         | Not_coherent_metas ->
-          apply_one_mhyp_context_rec mhyp lhyps_acc (nocc + 1) ((id,hyp)::tl)))
-    | [] -> raise No_match in
+          apply_one_mhyp_context_rec ist env mhyp lhyps_acc (nocc + 1)
+                                     ((id,hyp)::tl)))
+    | [] ->
+      begin
+        db_hyp_pattern_failure ist.debug env (get_info_pattern mhyp);
+        raise No_match
+      end in
   let nocc =
     match noccopt with
     | None -> 0
     | Some n -> n in
-  apply_one_mhyp_context_rec mhyp [] nocc lhyps
+  apply_one_mhyp_context_rec ist env mhyp [] nocc lhyps
+
+(* Gets the identifier of the pattern if it exists *)
+let get_id_pattern = function
+  | [] -> None
+  | [(id,_)] -> Some id
+  | _ -> assert false
+
+(*
+let coerce_to_qualid loc = function
+  | Constr c when isVar c -> make_short_qualid (destVar c)
+  | Constr c -> 
+      (try qualid_of_sp (sp_of_global (Global.env()) (reference_of_constr c))
+      with Not_found -> invalid_arg_loc (loc, "Not a reference"))
+  | Identifier id -> make_short_qualid id
+  | Qualid qid -> qid
+  | _ -> invalid_arg_loc (loc, "Not a reference")
+*)
 
 let constr_to_id loc c =
   if isVar c then destVar c
@@ -884,6 +922,9 @@ let hyp_or_metanum_interp ist gl = function
   | AN id -> eval_variable ist gl (dummy_loc,id)
   | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lmatch)
 
+(* To avoid to move to much simple functions in the big recursive block *)
+let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented")
+
 let interp_pure_qualid is_applied env (loc,qid) =
   try VConstr (constr_of_reference (find_reference env qid))
   with Not_found ->
@@ -1072,12 +1113,12 @@ let rec val_interp ist gl tac =
     | TacArg a -> tacarg_interp ist gl a
     (* Delayed evaluation *)
     | t -> VTactic (eval_tactic ist t)
-
- in
+  in 
   match ist.debug with
-    | DebugOn n ->
-	debug_prompt n (Some gl) tac (fun v -> value_interp {ist with debug=v})
-    | _ -> value_interp ist
+  | DebugOn | Run _ ->
+    let debug = debug_prompt gl ist.debug tac in
+    value_interp {ist with debug=debug}
+  | _ -> value_interp ist
 
 and eval_tactic ist = function
   | TacAtom (loc,t) -> fun gl ->
@@ -1176,7 +1217,7 @@ and eval_with_fail interp tac goal =
     | a -> a)
   with | FailError lvl ->
     if lvl = 0 then
-      raise No_match
+      raise Eval_fail
     else
       raise (FailError (lvl - 1))
 
@@ -1200,7 +1241,6 @@ and letin_interp ist gl = function
       let v = tacarg_interp ist gl t in
       check_is_value v;
       (id,v):: (letin_interp ist gl tl)
-
   | ((loc,id),Some com,tce)::tl ->
     let typ = interp_may_eval pf_interp_constr ist gl com
     and v = tacarg_interp ist gl tce in
@@ -1248,14 +1288,9 @@ and letcut_interp ist = function
     and exat = h_exact csr in
     tclTHENSV cutt [|tclTHEN (introduction id) (letcut_interp ist tl);exat|] gl
 
-(*      let lic = mkLetIn (Name id,csr,typ,ccl) in
-      let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in
-      tclTHEN ntac (tclTHEN (introduction id)
-      (letcut_interp ist tl))*)
-
 (* Interprets the Match Context expressions *)
-and match_context_interp ist goal lr lmr =
-  let rec apply_goal_sub ist nocc (id,c) csr mt mhyps hyps =
+and match_context_interp ist g lr lmr =
+  let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
     try
       let (lgoal,ctxt) = sub_match nocc c csr in
       let lctxt = give_context ctxt id in
@@ -1264,18 +1299,23 @@ and match_context_interp ist goal lr lmr =
           (val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch})
           mt goal
       else
-        apply_hyps_context ist goal mt lgoal mhyps hyps
+        apply_hyps_context ist env goal mt lgoal mhyps hyps
     with
     | (FailError _) as e -> raise e
     | NextOccurrence _ -> raise No_match
     | e when e = No_match or Logic.catchable_exception e ->
-      apply_goal_sub ist (nocc + 1) (id,c) csr mt mhyps hyps in
-  let rec apply_match_context ist = function
+      apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
+  let rec apply_match_context ist env goal nrs lex lpt = 
+    begin
+    if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
+    match lpt with
     | (All t)::tl ->
-      (try
-         eval_with_fail (val_interp ist) t goal
-       with No_match | FailError _ -> apply_match_context ist tl
-	 | e when Logic.catchable_exception e -> apply_match_context ist tl)
+      begin
+        db_mc_pattern_success ist.debug;
+        try eval_with_fail (val_interp ist) t goal
+         with e when is_match_catchable e ->
+           apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+      end
     | (Pat (mhyps,mgoal,mt))::tl ->
       let hyps = make_hyps (pf_hyps goal) in
       let hyps = if lr then List.rev hyps else hyps in
@@ -1288,63 +1328,77 @@ and match_context_interp ist goal lr lmr =
             begin
             db_matched_concl ist.debug (pf_env goal) concl;
             if mhyps = [] then
-              eval_with_fail
-		(val_interp {ist with lmatch=lgoal@ist.lmatch}) mt goal
+            begin
+              db_mc_pattern_success ist.debug;
+              eval_with_fail (val_interp
+                {ist with lmatch=lgoal@ist.lmatch}) mt goal
+            end
             else
-              apply_hyps_context ist goal mt lgoal mhyps hyps
+              apply_hyps_context ist env goal mt lgoal mhyps hyps
             end)
-        with e when is_match_catchable e -> apply_match_context ist tl)
+        with 
+        | e when is_match_catchable e ->
+          begin 
+            (match e with
+            | No_match -> db_matching_failure ist.debug
+            | Eval_fail -> db_eval_failure ist.debug
+            | _ -> db_logic_failure ist.debug e);
+            apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+          end)
       |	Subterm (id,mg) ->
-        (try
-          apply_goal_sub ist 0 (id,mg) concl mt mhyps hyps
-        with e when is_match_catchable e ->
-	  apply_match_context ist tl))
+        (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
+         with e when is_match_catchable e ->
+           apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
     | _ ->
-      errorlabstrm "Tacinterp.apply_match_context" (str
-        "No matching clauses for Match Context")
-
-  in
-  let env = pf_env goal in
-  apply_match_context ist 
-    (read_match_rule (project goal) env (constr_list ist env) lmr)
+      errorlabstrm "Tacinterp.apply_match_context"
+        (v 0 (str "No matching clauses for Match Context" ++
+        (if ist.debug=DebugOff then
+           fnl() ++ str "(use \"Debug On\" for more info)"
+         else mt())))
+    end in
+  let env = pf_env g in
+  apply_match_context ist env g 0 lmr
+    (read_match_rule (project g) env (constr_list ist env) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context ist goal mt lgmatch mhyps hyps =
-  let rec apply_hyps_context_rec mt lfun lmatch mhyps lhyps_mhyp
+and apply_hyps_context ist env goal mt lgmatch mhyps hyps =
+  let rec apply_hyps_context_rec ist 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 goal lmatch hd lhyps_mhyp noccopt in
+          apply_one_mhyp_context ist env goal lmatch hd lhyps_mhyp noccopt in
         begin
-        db_matched_hyp ist.debug (pf_env goal) hyp_match;
-        (try
-        if tl = [] then
-            eval_with_fail
-              (val_interp {ist with lfun=lfun@lid@lc@ist.lfun;
-                                    lmatch=lmatch@lm@ist.lmatch})
-              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 mt
-            (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
-         with
-        | (FailError _) as e -> raise e
-	|  e when is_match_catchable e -> 
-          (match noccopt with
-          | None ->
-            apply_hyps_context_rec mt lfun
-              lmatch mhyps newlhyps lhyps_rest None
-          | Some nocc ->
-            apply_hyps_context_rec mt ist.lfun ist.lmatch mhyps
-              (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1))))
+          db_matched_hyp ist.debug (pf_env goal) hyp_match
+                         (get_id_pattern lid);
+          (try
+          if tl = [] then
+          begin
+            db_mc_pattern_success ist.debug;
+            eval_with_fail (val_interp {ist with lfun=lfun@lid@lc@ist.lfun;
+                                        lmatch=lmatch@lm@ist.lmatch}) mt goal
+          end
+          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 ist mt
+              (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None
+           with
+           | (FailError _) as e -> raise e
+	   | e when is_match_catchable e -> 
+             (match noccopt with
+             | None ->
+               apply_hyps_context_rec ist mt lfun
+                 lmatch mhyps newlhyps lhyps_rest None
+             | Some nocc ->
+               apply_hyps_context_rec ist mt ist.lfun ist.lmatch mhyps
+                 (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1))))
         end
       |	[] ->
         anomalylabstrm "apply_hyps_context_rec" (str
           "Empty list should not occur") in
-  apply_hyps_context_rec mt [] lgmatch mhyps hyps hyps None
+  apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None
 
   (* Interprets extended tactic generic arguments *)
 and genarg_interp ist goal x =
@@ -1517,7 +1571,8 @@ and interp_atomic ist gl = function
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      h_reduce (pf_redexp_interp ist gl r) (List.map (interp_hyp_location ist gl) cl)
+      h_reduce (pf_redexp_interp ist gl r) (List.map
+               (interp_hyp_location ist gl) cl)
   | TacChange (occl,c,cl) ->
       h_change (option_app (pf_pattern_interp ist gl) occl)
         (pf_constr_interp ist gl c) (List.map (interp_hyp_location ist gl) cl)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 129794c587..45fe9995ef 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -115,6 +115,8 @@ let rec explain_exn_default = function
 let raise_if_debug e =
   if !Options.debug then raise e
 
+let _ = Tactic_debug.explain_logic_error := explain_exn_default
+
 let explain_exn_function = ref explain_exn_default
 
 let explain_exn e = !explain_exn_function e
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6a282d5477..ef5430e3b9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1036,7 +1036,7 @@ let vernac_check_guard () =
   msgnl message
 
 let vernac_debug b =
-  set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
+  set_debug (if b then Tactic_debug.DebugOn else Tactic_debug.DebugOff)
 
 
 (**************************)