From 401f17afa2e9cc3f2d734aef0d71a2c363838ebd Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 2 Mar 2012 22:30:29 +0000
Subject: Noise for nothing

Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.

+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'proofs/proof.ml')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 871e68acfc..42a522b7c8 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -102,7 +102,7 @@ end
 exception CannotUnfocusThisWay
 let _ = Errors.register_handler begin function
   | CannotUnfocusThisWay ->
-    Util.error "This proof is focused, but cannot be unfocused this way"
+    Errors.error "This proof is focused, but cannot be unfocused this way"
   | _ -> raise Errors.Unhandled
 end
 
@@ -184,7 +184,7 @@ let push_focus cond inf context pr =
 
 exception FullyUnfocused
 let _ = Errors.register_handler begin function
-  | FullyUnfocused -> Util.error "The proof is not focused"
+  | FullyUnfocused -> Errors.error "The proof is not focused"
   | _ -> raise Errors.Unhandled
 end
 (* An auxiliary function to read the kind of the next focusing step *)
@@ -211,7 +211,7 @@ let push_undo save pr =
 (* Auxiliary function to pop and read a [save_state] from the undo stack. *)
 exception EmptyUndoStack
 let _ = Errors.register_handler begin function
-  | EmptyUndoStack -> Util.error "Cannot undo: no more undo information"
+  | EmptyUndoStack -> Errors.error "Cannot undo: no more undo information"
   | _ -> raise Errors.Unhandled
 end
 let pop_undo pr =
@@ -387,8 +387,8 @@ let start goals =
 exception UnfinishedProof
 exception HasUnresolvedEvar
 let _ = Errors.register_handler begin function
-  | UnfinishedProof -> Util.error "Some goals have not been solved."
-  | HasUnresolvedEvar -> Util.error "Some existential variables are uninstantiated."
+  | UnfinishedProof -> Errors.error "Some goals have not been solved."
+  | HasUnresolvedEvar -> Errors.error "Some existential variables are uninstantiated."
   | _ -> raise Errors.Unhandled
 end
 let return p =
-- 
cgit v1.2.3