diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-31 14:26:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-31 14:26:27 +0200 |
| commit | 842dfef1d52c739119808ea1dec3509c0cf86435 (patch) | |
| tree | 072d78acd19daa086183b2431220e3701836ce56 /grammar | |
| parent | b3485ddc8c4f98743426bb58c8d49b76edd43d61 (diff) | |
| parent | 91ee24b4a7843793a84950379277d92992ba1651 (diff) | |
This patch splits pretty printing representation from IO operations.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 4 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 8593bad5d..ae6d2d18e 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -117,7 +117,7 @@ let declare_tactic loc s c cl = match cl with Tacenv.register_ml_tactic $se$ [|$tac$|]; Mltop.declare_cache_obj obj $plugin_name$; } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in tactic extend " ^ $entry$ ^": ")) (Errors.print e)) ]; } >> @@ -135,7 +135,7 @@ let declare_tactic loc s c cl = match cl with Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc s cl$); Mltop.declare_cache_obj $obj$ $plugin_name$; } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in tactic extend " ^ $entry$ ^": ")) (Errors.print e)) ]; } >> diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 1611de39c..215d27dbd 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -128,7 +128,7 @@ let declare_command loc s c nt cl = CList.iteri (fun i (depr, f) -> Vernacinterp.vinterp_add depr ($se$, i) f) $funcl$; CList.iteri (fun i f -> Vernac_classifier.declare_vernac_classifier ($se$, i) f) $classl$ } with [ e when Errors.noncritical e -> - Pp.msg_warning + Feedback.msg_warning (Pp.app (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) (Errors.print e)) ]; |