aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-06-10 19:27:58 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-06-11 15:42:51 +0200
commite781fdf9a135526e67ebb014412c663d54ef9e28 (patch)
tree578749aaabf171755af31353534014d56cdb3dad /plugins/setoid_ring
parent06d4250ec3a62b74c41a4f41deb65e97962f8850 (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.v4
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).