summaryrefslogtreecommitdiff
path: root/ide/coq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.ml')
-rw-r--r--ide/coq.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 1c6229b4..1a5b9def 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
+(* $Id: coq.ml 15025 2012-03-09 14:27:07Z glondu $ *)
open Vernac
open Vernacexpr
@@ -112,7 +112,7 @@ let is_in_proof_mode () =
| _ -> true
let user_error_loc l s =
- raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
+ raise (Compat.Exc_located (l, Util.UserError ("CoqIde", s)))
type printing_state = {
mutable printing_implicit : bool;
@@ -443,7 +443,7 @@ let interp_and_replace s =
let rec is_pervasive_exn = function
| Out_of_memory | Stack_overflow | Sys.Break -> true
| Error_in_file (_,_,e) -> is_pervasive_exn e
- | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
+ | Compat.Exc_located (_,e) -> is_pervasive_exn e
| DuringCommandInterp (_,e) -> is_pervasive_exn e
| _ -> false
@@ -456,7 +456,7 @@ let print_toplevel_error exc =
in
let (loc,exc) =
match exc with
- | Stdpp.Exc_located (loc, ie) -> (Some loc),ie
+ | Compat.Exc_located (loc, ie) -> (Some loc),ie
| Error_in_file (s, (_,fname, loc), ie) -> None, ie
| _ -> dloc,exc
in