Misc fixes related to new nsatz (and ocamlbuild)

 - Kill a warning in ideal.ml corresponding to really brain-dead code.
 - Restore extraction/vo.otarget in pluginsvo.itarget
 - In fact, plugins/_tags can be merged into _tags with nice ** patterns
 - Update .gitignore

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13062 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 6 insertions, 56 deletions

diff --git a/plugins/_tags b/plugins/_tags
deleted file mode 100644
index 8cf17e02a8..0000000000
--- a/plugins/_tags
+++ /dev/null
@@ -1,42 +0,0 @@
-
-"romega/g_romega.ml4": use_grammar
-"cc/g_congruence.ml4": use_grammar
-"setoid_ring/newring.ml4": use_grammar
-"dp/g_dp.ml4": use_grammar
-"quote/g_quote.ml4": use_grammar
-"subtac/equations.ml4": use_grammar
-"subtac/g_eterm.ml4": use_grammar
-"subtac/g_subtac.ml4": use_grammar
-"rtauto/g_rtauto.ml4": use_grammar
-"xml/xmlentries.ml4": use_grammar
-"xml/dumptree.ml4": use_grammar
-"firstorder/g_ground.ml4": use_grammar
-"omega/g_omega.ml4": use_grammar
-"micromega/g_micromega.ml4": use_grammar
-"funind/g_indfun.ml4": use_grammar
-"field/field.ml4": use_grammar
-"extraction/g_extraction.ml4": use_grammar
-"ring/g_ring.ml4": use_grammar
-"fourier/g_fourier.ml4": use_grammar
-"groebner/groebner.ml4": use_grammar
-"decl_mode/g_decl_mode.ml4": use_grammar
-
-"cc": include
-"decl_mode": include
-"extraction": include
-"firstorder": include
-"funind": include
-"micromega": include
-"quote": include
-"romega": include
-"setoid_ring": include
-"xml": include
-"dp": include
-"field": include
-"fourier": include
-"groebner": include
-"jprover": include
-"omega": include
-"ring": include
-"rtauto": include
-"subtac": include
\ No newline at end of file
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index b4a0e7ade6..b91f01d1c1 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -875,9 +875,6 @@ let critere3 ((i,j),m) lp lcp =
 
 let add_cpairs p lp lcp =
   mergecpairs (cpairs1 p lp) lcp 
-   
-let prod_rec f = function
-    (x0, x) -> f x0 x
 
 let step = ref 0
 
@@ -950,9 +947,6 @@ let divide_rem_with_critical_pair = ref false
 let list_diff l x =
   filter (fun y -> y <> x) l
 
-let choix_spol p l =
-  l
-
 let deg_hom p =
   match p with
   | [] -> -1
@@ -962,9 +956,8 @@ let pbuchf pq p lp0=
   info "computation of the Groebner basis\n";
   step:=0;
   Hashtbl.clear hmon;
-  let rec pbuchf x = 
-    prod_rec (fun lp lpc ->
-      infobuch lp lpc; 
+  let rec pbuchf (lp, lpc) =
+      infobuch lp lpc;
 (*      step:=(!step+1)mod 10;*)
       match lpc with
         [] ->
@@ -972,8 +965,7 @@ let pbuchf pq p lp0=
 	 (* info ("List of polynomials:\n"^(fold_left (fun r p -> r^(stringP p)^"\n") "" lp));
 	  info "--------------------\n";*)
 	  test_dans_ideal (ppol p) lp lp0
-      | _ ->
-	  let (((i,j),m)::lpc2)= choix_spol !pol_courant lpc in
+      | ((i,j),m) :: lpc2 ->
 (*          info "choosen pair\n";*)
 	  if critere3 ((i,j),m) lp lpc2
 	  then (info "c"; pbuchf (lp, lpc2))
@@ -1009,9 +1001,8 @@ let pbuchf pq p lp0=
 		  try test_dans_ideal (ppol p) (addS a0 lp) lp0
 		  with NotInIdeal ->
 		    let newlpc = add_cpairs a0 lp lpc2 in
-		    pbuchf (((addS a0 lp), newlpc)))
-      x
-  in pbuchf pq 
+		    pbuchf (((addS a0 lp), newlpc))
+  in pbuchf pq
     
 let is_homogeneous p =
   match p with
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
index 033d1a199c..db56534c98 100644
--- a/plugins/pluginsvo.itarget
+++ b/plugins/pluginsvo.itarget
@@ -10,3 +10,4 @@ ring/vo.otarget
 romega/vo.otarget
 rtauto/vo.otarget
 setoid_ring/vo.otarget
+extraction/vo.otarget
\ No newline at end of file