diff options
Diffstat (limited to 'toplevel/cerrors.mli')
| -rw-r--r-- | toplevel/cerrors.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli index cd6ccd565..a67c887af 100644 --- a/toplevel/cerrors.mli +++ b/toplevel/cerrors.mli @@ -9,10 +9,6 @@ (** Toplevel Exception *) exception EvaluatedError of Pp.std_ppcmds * exn option -(** Error report. *) - -val print_loc : Loc.t -> Pp.std_ppcmds - (** Pre-explain a vernac interpretation error *) val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> Util.iexn -> Util.iexn |