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

1 files changed, 1 insertions, 1 deletions

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index a8c79c31e..02503ab47 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";