diff options
| -rw-r--r-- | grammar/tacextend.ml4 | 6 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 11 |
2 files changed, 13 insertions, 4 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 8f70302a0d..41c3676896 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -189,7 +189,11 @@ let declare_tactic loc s cl = Tacexpr.TacExtend($default_loc$,$se$,l))) | None -> () ]) $atomic_tactics$ - with e -> Pp.pp (Errors.print e); + with e -> + Pp.msg_warning + (Stream.iapp + (Pp.str ("Exception in tactic extend " ^ $se$ ^": ")) + (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 8ec189e3d1..2c9bc2675a 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -50,13 +50,18 @@ let mlexpr_of_clause = (Option.List.cons (Option.map (fun a -> GramTerminal a) a) b)) let declare_command loc s nt cl = + let se = mlexpr_of_string s in let gl = mlexpr_of_clause cl in let funcl = make_fun_clauses loc s cl in declare_str_items loc [ <:str_item< do { - try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$ - with e -> Pp.pp (Errors.print e); - Egramml.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$ + try Vernacinterp.vinterp_add $se$ $funcl$ + with e -> + Pp.msg_warning + (Stream.iapp + (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) + (Errors.print e)); + Egramml.extend_vernac_command_grammar $se$ $nt$ $gl$ } >> ] open Pcaml |