diff options
Diffstat (limited to 'grammar/vernacextend.mlp')
| -rw-r--r-- | grammar/vernacextend.mlp | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index ce0431889..04b117fba 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -122,14 +122,8 @@ let declare_command loc s c nt cl = let classl = make_fun_classifiers loc s c cl in declare_str_items loc [ <:str_item< do { - try do { - 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 -> - Feedback.msg_warning - (Pp.app - (Pp.str ("Exception in vernac extend " ^ $se$ ^": ")) - (Errors.print e)) ]; + 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$; CList.iteri (fun i r -> Egramml.extend_vernac_command_grammar ($se$, i) $nt$ r) $gl$; } >> ] |