diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | _tags | 4 | ||||
| -rw-r--r-- | plugins/_tags | 42 | ||||
| -rw-r--r-- | plugins/nsatz/ideal.ml | 19 | ||||
| -rw-r--r-- | plugins/pluginsvo.itarget | 1 |
5 files changed, 11 insertions, 57 deletions
diff --git a/.gitignore b/.gitignore index 98479902a..0fae2539b 100644 --- a/.gitignore +++ b/.gitignore @@ -139,7 +139,7 @@ plugins/field/field.ml plugins/funind/g_indfun.ml plugins/omega/g_omega.ml plugins/quote/g_quote.ml -plugins/groebner/groebner.ml +plugins/nsatz/nsatz.ml plugins/micromega/g_micromega.ml plugins/subtac/g_subtac.ml plugins/fourier/g_fourier.ml @@ -35,6 +35,8 @@ "tactics/hipattern.ml4": use_grammar, use_constr "tactics/rewrite.ml4": use_grammar +<plugins/**/*.ml4>: use_grammar + ## sub-directory inclusion # Note: "checker" is deliberately not included @@ -59,3 +61,5 @@ "tools": include "tools/coqdoc": include "toplevel": include + +<plugins/**>: include
\ No newline at end of file diff --git a/plugins/_tags b/plugins/_tags deleted file mode 100644 index 8cf17e02a..000000000 --- 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 b4a0e7ade..b91f01d1c 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 033d1a199..db56534c9 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 |