From d030c8f18316d63c1d9bda68448ccc70187694f6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Nov 2003 00:00:33 +0000
Subject: Protection contre les buts sans inegalite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4767 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/fourier/fourierR.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 8da7530ea0..1fae97ef02 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -496,9 +496,10 @@ let rec fourier gl=
                         (list_of_sign (pf_hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
-		        with _-> ())
+		        with _ -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
+    if !lineq=[] then Util.error "No inequalities";
     let res=fourier_lineq (!lineq) in
     let tac=ref tclIDTAC in
     if res=[]
-- 
cgit v1.2.3