From a49d610f95a9d78d273cc34a82cc91ebfab2f22a Mon Sep 17 00:00:00 2001
From: bertot
Date: Mon, 28 Aug 2006 11:42:14 +0000
Subject: improve the amount of information given by the Ltac tactic debugger

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tactic_debug.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 889e06a8b5..96df8f6418 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -31,6 +31,8 @@ type debug_info =
 (* An exception handler *)
 let explain_logic_error = ref (fun e -> mt())
 
+let explain_logic_error_no_anomaly = ref (fun e -> mt())
+
 (* Prints the goal *)
 let db_pr_goal g =
   msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Refiner.sig_it g))
-- 
cgit v1.2.3