diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-10 19:27:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-11 15:42:51 +0200 |
| commit | e781fdf9a135526e67ebb014412c663d54ef9e28 (patch) | |
| tree | 578749aaabf171755af31353534014d56cdb3dad /plugins/setoid_ring | |
| parent | 06d4250ec3a62b74c41a4f41deb65e97962f8850 (diff) | |
In generalized rewrite, avoid retyping completely and constantly the conclusion, and results of
unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x
speedup in Ncring_polynom.
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). |