From d028f9233d7cca269485eff20a06cfab2e98acf7 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sun, 17 Mar 2013 22:00:35 +0000
Subject: Fix some camlp5 quotations , restoring compatibility with camlp5 5.x

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

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 23cf41bb21..2972651a9e 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -168,11 +168,11 @@ let declare_tactic loc s cl =
                  Tacexpr.TacExtend($default_loc$,$se$,l)))
            | None -> () ])
           $atomic_tactics$
-      with e when Errors.noncritical e ->
+      with [ e when Errors.noncritical e ->
 	Pp.msg_warning
 	  (Pp.app
 	     (Pp.str ("Exception in tactic extend " ^ $se$ ^": "))
-	     (Errors.print e));
+	     (Errors.print e)) ];
       Egramml.extend_tactic_grammar $se$ $gl$;
       List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
     ]
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index b9b9dd8ead..7d02a1ba5e 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -55,11 +55,11 @@ let declare_command loc s nt cl =
   declare_str_items loc
     [ <:str_item< do {
 	try Vernacinterp.vinterp_add $se$ $funcl$
-	with e when Errors.noncritical e ->
+	with [ e when Errors.noncritical e ->
 	  Pp.msg_warning
 	    (Pp.app
 	       (Pp.str ("Exception in vernac extend " ^ $se$ ^": "))
-	       (Errors.print e));
+	       (Errors.print e)) ];
 	Egramml.extend_vernac_command_grammar $se$ $nt$ $gl$
       } >> ]
 
-- 
cgit v1.2.3