Permalink
Browse files

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
  • Loading branch information...
letouzey
letouzey committed Mar 17, 2013
1 parent 70d582a commit d028f9233d7cca269485eff20a06cfab2e98acf7
Showing with 4 additions and 4 deletions.
  1. +2 −2 grammar/tacextend.ml4
  2. +2 −2 grammar/vernacextend.ml4
View
@@ -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$; } >>
]
View
@@ -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$
} >> ]

0 comments on commit d028f92

Please sign in to comment.