Fixing a significant efficiency leak in the code of the field tactic.

The field tactic post-processes the data generated during normalization
to ensure that vanished denominators do not cancel: essentially, this
step removes duplicates from a list of polynomials and uses the
clean list to generate the conjunction of associated non-zero conditions. This
conjunction is the proof obligation the user has to prove by hand after
a successful call to the field tactic.

The computation of the proof obligation statement
was performed using a fine-tuned reduction strategy, coded in
the newring.ml4 file (see the fv-protect tactic).
However, not only this strategy information was forgotten by the kernel,
but the strategy used at Qed time caused a real explosion (examples
normalized in 70s by the tactic have a one hour Qed). No idea why.

The fix consists in opacifying the part of the goal irrelevant to
computation and call the vm on the duplicate removal step. BTW this step 
is programmed in a naive way and can probably be made more efficient.



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

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index d584adfc8..52b632a7d 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1395,14 +1395,14 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
   end.
 
 Lemma fcons_ok : forall l l1,
-  PCond l (Fapp l1 nil) -> PCond l l1.
+  (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1.
+intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1.
 Proof.
 induction l1; simpl; intros.
  trivial.
  elim PCond_fcons_inv with (1 := H); intros.
  destruct l1; trivial. split; trivial. apply IHl1; trivial.
 Qed.
-
 End Fcons_impl.
 
 Section Fcons_simpl.