diff options
Diffstat (limited to 'contrib/setoid_ring/Ring_polynom.v')
| -rw-r--r-- | contrib/setoid_ring/Ring_polynom.v | 2 |
1 files changed, 2 insertions, 0 deletions
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. |