diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-12 09:36:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-12 09:36:51 +0200 |
| commit | ce2ce8f2c302e538514ecb48b0a8c41bdcb80124 (patch) | |
| tree | 293dbb546beecc2bb738d177b7fae99f2c272d84 /test-suite/typeclasses | |
| parent | 8059a0efa79fcd72d56c424adf1bea10dae28d6d (diff) | |
Attempt to fix the doubly encapsulated Ltac errors in coqide.
It seems that ExplainErr.process_vernac_interp_error is called twice
in CoqIDE. First time in Stm.stm_vernac_interp (via
Stm.call_process_error_once). Second time in the "handle_exn" method
used by CoqIDE to handle exceptions coming from Coq
(ide_slave.ml/xmlprotocol.ml).
The proposed fix is to remove the call in CoqIDE, assuming that the
process_vernac_interp_error call is done otherwise on all potential
error paths.
Diffstat (limited to 'test-suite/typeclasses')
0 files changed, 0 insertions, 0 deletions