aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/_tags42
-rw-r--r--plugins/nsatz/ideal.ml19
-rw-r--r--plugins/pluginsvo.itarget1
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