5 files changed, 53 insertions, 53 deletions

diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index d6447111..f37d0027 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Fourier.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* "Fourier's method to solve linear inequations/equations systems.".*)
 
 Require Export LegacyRing.
diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
index 7c5b5ed7..b10c304c 100644
--- a/plugins/fourier/Fourier_util.v
+++ b/plugins/fourier/Fourier_util.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Fourier_util.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Export Rbase.
 Comments "Lemmas used by the tactic Fourier".
 
@@ -18,7 +16,7 @@ intros; apply Rmult_lt_compat_l; assumption.
 Qed.
 
 Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1.
-red in |- *.
+red.
 intros.
 case H; auto with real.
 Qed.
@@ -65,19 +63,19 @@ Lemma Rfourier_le_le :
    x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2.
 intros x1 y1 x2 y2 a H H0 H1; try assumption.
 case H0; intros.
-red in |- *.
+red.
 left; try assumption.
 apply Rfourier_le_lt; auto with real.
 rewrite H2.
 case H; intros.
-red in |- *.
+red.
 left; try assumption.
 rewrite (Rplus_comm x1 (a * y2)).
 rewrite (Rplus_comm y1 (a * y2)).
 apply Rplus_lt_compat_l.
 try exact H3.
 rewrite H3.
-red in |- *.
+red.
 right; try assumption.
 auto with real.
 Qed.
@@ -86,7 +84,7 @@ Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x.
 intros x H; try assumption.
 rewrite Rplus_comm.
 apply Rle_lt_0_plus_1.
-red in |- *; auto with real.
+red; auto with real.
 Qed.
 
 Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y.
@@ -103,12 +101,12 @@ Qed.
 Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x.
 intros x H; try assumption.
 case H; intros.
-red in |- *.
+red.
 left; try assumption.
 apply Rlt_zero_pos_plus1; auto with real.
 rewrite <- H0.
 replace (1 + 0) with 1.
-red in |- *; left.
+red; left.
 exact Rlt_zero_1.
 ring.
 Qed.
@@ -116,28 +114,28 @@ Qed.
 Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y.
 intros x y H H0; try assumption.
 case H; intros.
-red in |- *; left.
+red; left.
 apply Rlt_mult_inv_pos; auto with real.
 rewrite <- H1.
-red in |- *; right; ring.
+red; right; ring.
 Qed.
 
 Lemma Rle_zero_1 : 0 <= 1.
-red in |- *; left.
+red; left.
 exact Rlt_zero_1.
 Qed.
 
 Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d.
-intros n d H; red in |- *; intros H0; try exact H0.
+intros n d H; red; intros H0; try exact H0.
 generalize (Rgt_not_le 0 (n * / d)).
 intros H1; elim H1; try assumption.
 replace (n * / d) with (- - (n * / d)).
 replace 0 with (- -0).
 replace (- (n * / d)) with (- n * / d).
 replace (-0) with 0.
-red in |- *.
+red.
 apply Ropp_gt_lt_contravar.
-red in |- *.
+red.
 exact H0.
 ring.
 ring.
@@ -164,7 +162,7 @@ ring.
 Qed.
 
 Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y.
-unfold not in |- *; intros.
+unfold not; intros.
 apply H.
 apply Rplus_lt_reg_r with x.
 replace (x + 0) with x.
@@ -175,7 +173,7 @@ ring.
 Qed.
 
 Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y.
-unfold not in |- *; intros.
+unfold not; intros.
 apply H.
 case H0; intros.
 left.
@@ -190,7 +188,7 @@ rewrite H1; ring.
 Qed.
 
 Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y.
-unfold Rgt in |- *; intros; assumption.
+unfold Rgt; intros; assumption.
 Qed.
 
 Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y.
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 1a92c716..1574e21e 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: fourier.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* Méthode d'élimination de Fourier *)
 (* Référence:
 Auteur(s) : Fourier, Jean-Baptiste-Joseph
@@ -177,7 +175,7 @@ let unsolvable lie =
 			raise (Failure "contradiction found"))
           |_->assert false)
 			     lr)
-   with _ -> ());
+   with e when Errors.noncritical e -> ());
    !res
 ;;
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 2cabcf52..e0e4f7d6 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: fourierR.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 
 
 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
@@ -31,17 +29,23 @@ qui donne le coefficient d'un terme du calcul des constructions,
 qui est zéro si le terme n'y est pas.
 *)
 
-type flin = {fhom:(constr , rational)Hashtbl.t;
+module Constrhash = Hashtbl.Make
+  (struct type t = constr
+	  let equal = eq_constr
+	  let hash = hash_constr
+   end)
+
+type flin = {fhom: rational Constrhash.t;
              fcste:rational};;
 
-let flin_zero () = {fhom=Hashtbl.create 50;fcste=r0};;
+let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;
 
-let flin_coef f x = try (Hashtbl.find f.fhom x) with _-> r0;;
+let flin_coef f x = try (Constrhash.find f.fhom x) with Not_found -> r0;;
 
 let flin_add f x c =
     let cx = flin_coef f x in
-    Hashtbl.remove f.fhom x;
-    Hashtbl.add f.fhom x (rplus cx c);
+    Constrhash.remove f.fhom x;
+    Constrhash.add f.fhom x (rplus cx c);
     f
 ;;
 let flin_add_cste f c =
@@ -53,20 +57,20 @@ let flin_one () = flin_add_cste (flin_zero()) r1;;
 
 let flin_plus f1 f2 =
     let f3 = flin_zero() in
-    Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
-    Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
+    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
+    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
     flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
 ;;
 
 let flin_minus f1 f2 =
     let f3 = flin_zero() in
-    Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
-    Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
+    Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
+    Constrhash.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
     flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
 ;;
 let flin_emult a f =
     let f2 = flin_zero() in
-    Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
+    Constrhash.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
     flin_add_cste f2 (rmult a f.fcste);
 ;;
 
@@ -137,10 +141,12 @@ let rec flin_of_constr c =
 	     (try (let a=(rational_of_constr args.(0)) in
                      try (let b = (rational_of_constr args.(1)) in
 			    (flin_add_cste (flin_zero()) (rmult a b)))
-		     with _-> (flin_add (flin_zero())
+		     with e when Errors.noncritical e ->
+                       (flin_add (flin_zero())
 				 args.(1)
 				 a))
-	      with _-> (flin_add (flin_zero())
+	      with e when Errors.noncritical e ->
+                (flin_add (flin_zero())
 			  args.(0)
 			  (rational_of_constr args.(1))))
 	 | "Rinv"->
@@ -150,7 +156,8 @@ let rec flin_of_constr c =
 	     (let b=(rational_of_constr args.(1)) in
 		try (let a = (rational_of_constr args.(0)) in
 		       (flin_add_cste (flin_zero()) (rdiv a b)))
-		with _-> (flin_add (flin_zero())
+		with e when Errors.noncritical e ->
+                  (flin_add (flin_zero())
 		            args.(0)
                             (rinv b)))
          |_->assert false)
@@ -160,14 +167,15 @@ let rec flin_of_constr c =
               |"R0" -> flin_zero ()
               |_-> assert false)
   |_-> assert false)
-  with _ -> flin_add (flin_zero())
+  with e when Errors.noncritical e ->
+    flin_add (flin_zero())
                      c
 	             r1
 ;;
 
 let flin_to_alist f =
     let res=ref [] in
-    Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
+    Constrhash.iter (fun x c -> res:=(c,x)::(!res)) f;
     !res
 ;;
 
@@ -256,17 +264,17 @@ let ineq1_of_constr (h,t) =
 
 let fourier_lineq lineq1 =
    let nvar=ref (-1) in
-   let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
+   let hvar=Constrhash.create 50 in (* la table des variables des inéquations *)
    List.iter (fun f ->
-		Hashtbl.iter (fun x _ -> if not (Hashtbl.mem hvar x) then begin
+		Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin
 				nvar:=(!nvar)+1;
-				Hashtbl.add hvar x (!nvar)
+				Constrhash.add hvar x (!nvar)
 			      end)
                   f.hflin.fhom)
              lineq1;
    let sys= List.map (fun h->
                let v=Array.create ((!nvar)+1) r0 in
-               Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
+               Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c)
                   h.hflin.fhom;
                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
              lineq1 in
@@ -490,13 +498,13 @@ let rec fourier gl=
 	    |_->assert false)
         |_->assert false
       in tac gl)
-     with _ ->
+     with e when Errors.noncritical e ->
     (* les hypothèses *)
     let hyps = List.map (fun (h,t)-> (mkVar h,t))
                         (list_of_sign (pf_hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
-		        with _ -> ())
+		        with e when Errors.noncritical e -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
     if !lineq=[] then Util.error "No inequalities";
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index ea766830..7c7cf64f 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: g_fourier.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open FourierR
 
 TACTIC EXTEND fourier