diff options
| author | Emilio Jesus Gallego Arias | 2017-02-16 13:41:07 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-07 19:37:37 +0200 |
| commit | b209cea412a9541fd1c434dde36ea6eb1e256a33 (patch) | |
| tree | 1d9e19e84b3d2b6f6df127fd7a99ce4dace90069 /toplevel | |
| parent | 99c92fedebf629549eb16feb266f55c83ad99bd9 (diff) | |
[stm] remove process_error_hook
`process_error_hook` seems unnecesary, we just call the proper error
interpretation.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernac.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 9917a49b42..d5ceeaccd7 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -347,6 +347,3 @@ let compile v f = ignore(CoqworkmgrApi.get 1); compile v f; CoqworkmgrApi.giveback 1 - -let () = Hook.set Stm.process_error_hook - ExplainErr.process_vernac_interp_error |