diff options
| author |  Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-10-01 23:12:51 +0200 |
|---|---|---|
| committer | Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-10-01 23:15:34 +0200 |
| commit | b9a6247ddc52082065b56f296c889c41167e0507 (patch) | |
| tree | 616916af0ae9db831dbf6117a0d5564dd793c63f /plugins | |
| parent | c722207793eca59476152cc56329dc7a76ab0106 (diff) | |
Fix cbn behavior wrt simpl no match
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index 3e0e931b6..72f9f3e28 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. |