diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-04 23:26:36 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-04 23:26:36 +0000 |
| commit | 5ece01c8d71e2fdf7a87de71c342445599e137a0 (patch) | |
| tree | f13496a49ac9c94658d84031307b0c2022f26419 | |
| parent | abb4e7b0c1e8c0a5cc68052446333981379020d4 (diff) | |
Removed Compat.Exc_located outside of compat.ml4, as a consequence of
previous commit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16023 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/cerrors.ml | 8 | ||||
| -rw-r--r-- | toplevel/ide_slave.ml | 4 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 6 |
3 files changed, 0 insertions, 18 deletions
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index cc455dfeb..3739b0e4d 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -45,11 +45,6 @@ let explain_exn_default = function hov 0 ((if Loc.is_ghost loc then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ Errors.print_no_anomaly exc) - | Compat.Exc_located (loc, exc) -> - let loc = Compat.to_coqloc loc in - hov 0 ((if Loc.is_ghost loc then (mt ()) - else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) - ++ Errors.print_no_anomaly exc) | EvaluatedError (msg,None) -> msg | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise (* Otherwise, not handled here *) @@ -129,9 +124,6 @@ let rec process_vernac_interp_error = function Some (process_vernac_interp_error exc)) | Loc.Exc_located (loc,exc) -> Loc.Exc_located (loc,process_vernac_interp_error exc) - | Compat.Exc_located (loc, exc) -> - let loc = Compat.to_coqloc loc in - Loc.Exc_located (loc, process_vernac_interp_error exc) | exc -> exc diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index c12bbae7a..5c32bd0ed 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -290,10 +290,6 @@ let eval_call c = | Loc.Exc_located (loc, inner) -> let loc = if Loc.is_ghost loc then None else Some (Loc.unloc loc) in loc, pr_exn inner - | Compat.Exc_located (loc, inner) -> - let loc = Compat.to_coqloc loc in - let loc = if Loc.is_ghost loc then None else Some (Loc.unloc loc) in - loc, pr_exn inner | e -> None, pr_exn e in let interruptible f x = diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 479e14c8d..3a99d9df9 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -284,12 +284,6 @@ let print_toplevel_error exc = (print_highlight_location top_buffer loc, ie) else ((mt ()) (* print_command_location top_buffer dloc *), ie) - | Compat.Exc_located (loc, ie) -> - let loc = Compat.to_coqloc loc in - if valid_buffer_loc top_buffer dloc loc then - (print_highlight_location top_buffer loc, ie) - else - ((mt ()) (* print_command_location top_buffer dloc *), ie) | Error_in_file (s, (inlibrary, fname, loc), ie) -> (print_location_in_file s inlibrary fname loc, ie) | _ -> |