From b9a6247ddc52082065b56f296c889c41167e0507 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Wed, 1 Oct 2014 23:12:51 +0200 Subject: Fix cbn behavior wrt simpl no match --- plugins/setoid_ring/Ring_polynom.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins') diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 3e0e931b64..72f9f3e280 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -1049,10 +1049,10 @@ Section POWER. assert (H2 := norm_aux_PEopp pe2). rewrite norm_aux_PEadd. do 2 destruct get_PEopp; rewrite ?H1, ?H2; Esimpl; add_permut. - - simpl. rewrite IHpe1, IHpe2. Esimpl. - - simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok. - - simpl. rewrite IHpe. Esimpl. - - simpl. rewrite Ppow_N_ok by reflexivity. + - rewrite IHpe1, IHpe2. Esimpl. + - rewrite IHpe1, IHpe2. now rewrite Pmul_ok. + - rewrite IHpe. Esimpl. + - rewrite Ppow_N_ok by reflexivity. rewrite pow_th.(rpow_pow_N). destruct n0; simpl; Esimpl. induction p;simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. Qed. -- cgit v1.2.3