From e781fdf9a135526e67ebb014412c663d54ef9e28 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 10 Jun 2014 19:27:58 +0200 Subject: 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. --- plugins/setoid_ring/Ncring_polynom.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/setoid_ring/Ncring_polynom.v') 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). -- cgit v1.2.3