diff options
| author | letouzey | 2010-06-03 17:13:39 +0000 |
|---|---|---|
| committer | letouzey | 2010-06-03 17:13:39 +0000 |
| commit | 738af4011d12d253001d08384c4b7629834eaff9 (patch) | |
| tree | acc304563a7e10f9f0c5510df010f253c4e5592b | |
| parent | e6ed79dd304aae79277efa65e9398d7f27f69953 (diff) | |
Ide_blob: avoid direct use of Stdpp for compatibility with new camlp4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13063 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/ide_blob.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index 899cee1e46..81ad61930f 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -15,6 +15,7 @@ open Vernacexpr open Names +open Compat open Util open Pp open Printer @@ -256,7 +257,7 @@ let raw_interp s = Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string s,None)) let user_error_loc l s = - raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) + raise (Loc.Exc_located (l, Util.UserError ("CoqIde", s))) let interp verbosely s = prerr_endline "Starting interp..."; @@ -500,7 +501,7 @@ let init_stdout,read_stdout = let explain_exn e = let toploc,exc = match e with - | Stdpp.Exc_located (loc, inner) -> + | Loc.Exc_located (loc, inner) -> loc,inner | Error_in_file (s, (is_in_lib, fname, loc), inner) -> dummy_loc,inner |