diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacextend.ml | 24 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 9 |
2 files changed, 10 insertions, 23 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index e0afb7f483..5d38ea32be 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -92,28 +92,18 @@ let warn_deprecated_command = (* Interpretation of a vernac command *) let type_vernac opn converted_args ~atts = - let phase = ref "Looking up command" in - try - let depr, callback = vinterp_map opn in - let () = if depr then + let depr, callback = vinterp_map opn in + let () = if depr then let rules = Egramml.get_extend_vernac_rule opn in let pr_gram = function - | Egramml.GramTerminal s -> str s - | Egramml.GramNonTerminal _ -> str "_" + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" in let pr = pr_sequence pr_gram rules in warn_deprecated_command pr; - in - phase := "Checking arguments"; - let hunk = callback converted_args in - phase := "Executing command"; - hunk ~atts - with - | reraise -> - let reraise = Exninfo.capture reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - Exninfo.iraise reraise + in + let hunk = callback converted_args in + hunk ~atts (** VERNAC EXTEND registering *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 59557a60a6..280343f315 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -18,12 +18,9 @@ module Parser = struct let parse ps entry pa = Pcoq.unfreeze ps; - Flags.with_option Flags.we_are_parsing (fun () -> - try Pcoq.Entry.parse entry pa - with e when CErrors.noncritical e -> - let (e, info) = Exninfo.capture e in - Exninfo.iraise (e, info)) - () + Flags.with_option Flags.we_are_parsing + (fun () -> Pcoq.Entry.parse entry pa) + () end |