diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/Ncring_polynom.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 32824838b..b0348f8fd 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -216,8 +216,8 @@ Definition Psub(P P':Pol):= P ++ (--P'). intros l P i n Q;unfold mkPX. destruct P;try (simpl;reflexivity). assert (Hh := ring_morphism_eq c 0). -simpl; case_eq (Ceqb c 0);simpl;try reflexivity. -intros. + simpl; case_eq (Ceqb c 0);simpl;try reflexivity. + intros. rewrite Hh. rewrite ring_morphism0. rsimpl. apply Ceqb_eq. trivial. destruct (Pos.compare_spec i p). |