Imported Upstream version 8.4~betaupstream/8.4_beta

5 files changed, 26 insertions, 30 deletions

diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index d6447111..a1113d2d 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-2010     *)
 (*   \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..3d16f189 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-2010     *)
 (*   \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".
 
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 1a92c716..6c4d4d15 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-2010     *)
 (*   \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
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 2cabcf52..48493785 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-2010     *)
 (*   \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 _-> 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);
 ;;
 
@@ -167,7 +171,7 @@ let rec flin_of_constr c =
 
 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 +260,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
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index ea766830..9276eda1 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-2010     *)
 (*   \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