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/proofview.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'proofs/proofview.ml')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 4246cc9c7b..ff0e8de413 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -111,7 +111,7 @@ let focus_sublist i j l =
     try 
       Util.list_chop (j-i+1) sub_right 
     with Failure "list_chop" -> 
-      Util.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal")
+      Errors.errorlabstrm "nth_unproven" (Pp.str"No such unproven subgoal")
   in
   (sub, (left,right))
 
@@ -280,7 +280,7 @@ let tclFOCUS i j t env = { go = fun sk fk step ->
     is used otherwise. *)
 exception SizeMismatch
 let _ = Errors.register_handler begin function
-  | SizeMismatch -> Util.error "Incorrect number of goals."
+  | SizeMismatch -> Errors.error "Incorrect number of goals."
   | _ -> raise Errors.Unhandled
 end
 (* spiwack: we use an parametrised function to generate the dispatch tacticals.
@@ -316,7 +316,7 @@ let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step ->
     on with these exceptions. Does not catch anomalies. *)
 let purify t = 
   let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step
-     	                                                     with Util.Anomaly _ as e -> raise e
+     	                                                     with Errors.Anomaly _ as e -> raise e
 							           | e -> sk (Util.Inr e) fk step
 	       }
   in
@@ -400,7 +400,7 @@ let rec tclGOALBINDU s k =
 open Pretype_errors
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
-  | Util.UserError _
+  | Errors.UserError _
   | Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
   | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
@@ -505,9 +505,9 @@ module V82 = struct
     let (evk,_) = 
       let evl = Evarutil.non_instantiated pv.solution in
      if (n <= 0) then
-	Util.error "incorrect existential variable index"
+	Errors.error "incorrect existential variable index"
       else if List.length evl < n then
-	  Util.error "not so many uninstantiated existential variables"
+	  Errors.error "not so many uninstantiated existential variables"
       else
 	List.nth evl (n-1) 
     in
-- 
cgit v1.2.3