refined the conversion oracle

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

2 files changed, 4 insertions, 0 deletions

diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index f5c5504176..65a397acc6 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -661,6 +661,8 @@ Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R :=
   | FEpow x n => rpow (FEeval l x) (Cp_phi n)
   end.
 
+Strategy expand [FEeval].
+
 (* The result of the normalisation *)
  
 Record linear : Type := mk_linear {
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index 45b38e2edd..d88470369d 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -1186,6 +1186,8 @@ Proof.
    | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n)
    end.
 
+Strategy expand [PEeval].
+
  (** Correctness proofs *)
  
  Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l.