nouvelle version de la tactique groebner proposee par Loic:

- algo de Janet (finalement pas utilise)
- le hash-cons des certificats de Benjamin et Laurent pas encore integre
- traitement des puissances jusqu'a 6 (methode totalement naive)



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

1 files changed, 4 insertions, 0 deletions

diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index b31ebda55..0082eb9af 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -488,6 +488,10 @@ Ltac reduce_field_expr ope kont FLD fv expr :=
 
 (* Hack to let a Ltac return a term in the context of a primitive tactic *)
 Ltac return_term x := generalize (refl_equal x).
+Ltac get_term :=
+  match goal with 
+  | |- ?x = _ -> _ => x
+  end.
 
 (* Turn an operation on field expressions (FExpr) into a reduction
    on terms (in the field carrier). Because of field_lookup,