From 0ea545ef3301be9590d9a1ab7d3eee35d7caec92 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 11 Apr 2013 21:21:33 +0000
Subject: Backport r16394 from 8.4: - Fix caching of local hint database in
 typeclasses eauto which could miss some hypotheses. - Fix automatic solving
 of obligation in program, which was not trying to solve obligations that had
 no undefined dependencies left.

Fix a warning in fourierR.ml.


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

(limited to 'plugins')

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index a8c79c31e4..02503ab475 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -504,7 +504,7 @@ 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 NoIneq _ -> ())
+		        with NoIneq -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
     if !lineq=[] then Errors.error "No inequalities";
-- 
cgit v1.2.3