diff options
| author | Gaëtan Gilbert | 2019-07-08 13:07:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-08 13:07:30 +0200 |
| commit | a5e4dd7faa23abd4a4ebe093076484d090a8a47e (patch) | |
| tree | e0de245adb468dc3fe95d9108be749f010457365 /stm | |
| parent | 5ecfe31f9d900c6053531f2cb713035407009ba7 (diff) | |
| parent | 07abf9818a6b47bb2c2bd0a8201da9743a0c10b6 (diff) | |
Merge PR #9686: [error] Remove special error printing pre-processing
Reviewed-by: SkySkimmer
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 4db4579e38..9bbff476f8 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -120,13 +120,12 @@ let call = get let call_process_error_once = let processed : unit Exninfo.t = Exninfo.make () in - fun (_, info as ei) -> + fun (e, info) -> match Exninfo.get info processed with - | Some _ -> ei + | Some _ -> e, info | None -> - let e, info = ExplainErr.process_vernac_interp_error ei in - let info = Exninfo.add info processed () in - e, info + let info = Exninfo.add info processed () in + e, info end |