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
---
 plugins/fourier/fourierR.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/fourier')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 4849378583..1a629aac9a 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -503,11 +503,11 @@ let rec fourier gl=
 		        with _ -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
-    if !lineq=[] then Util.error "No inequalities";
+    if !lineq=[] then Errors.error "No inequalities";
     let res=fourier_lineq (!lineq) in
     let tac=ref tclIDTAC in
     if res=[]
-    then Util.error "fourier failed"
+    then Errors.error "fourier failed"
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
     else (match res with
         [(cres,sres,lc)]->
-- 
cgit v1.2.3