From 9aecb4427f0f8ca3cb4c26bc7f73bb74164a93d9 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 13 Mar 2013 00:00:17 +0000
Subject: Restrict (try...with...) to avoid catching critical exn (part 8)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 grammar/tacextend.ml4    | 2 +-
 grammar/vernacextend.ml4 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index e3e957d95c..23cf41bb21 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -168,7 +168,7 @@ let declare_tactic loc s cl =
                  Tacexpr.TacExtend($default_loc$,$se$,l)))
            | None -> () ])
           $atomic_tactics$
-      with e ->
+      with e when Errors.noncritical e ->
 	Pp.msg_warning
 	  (Pp.app
 	     (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 9ae529ea08..b9b9dd8ead 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -55,7 +55,7 @@ let declare_command loc s nt cl =
   declare_str_items loc
     [ <:str_item< do {
 	try Vernacinterp.vinterp_add $se$ $funcl$
-	with e ->
+	with e when Errors.noncritical e ->
 	  Pp.msg_warning
 	    (Pp.app
 	       (Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
-- 
cgit v1.2.3