From bbb941eb47625a07d36e0e45d6172cfa99bca027 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 May 2008 11:59:37 +0000 Subject: [PATCH] Dummy dependent types are no longer cleaned in inductive type arities. --- helm/software/matita/contribs/assembly/freescale/byte8.ma | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/contribs/assembly/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma index fd412e59e..f3d2e10b4 100644 --- a/helm/software/matita/contribs/assembly/freescale/byte8.ma +++ b/helm/software/matita/contribs/assembly/freescale/byte8.ma @@ -407,12 +407,12 @@ theorem plusb8nc_ok: generalize in match (plusb8_ok b1 b2 false); elim (plus_b8 b1 b2 false); simplify in H ⊢ %; - change with (nat_of_byte8 t = (b1 + b2) \mod 256); + change with (nat_of_byte8 a = (b1 + b2) \mod 256); rewrite < plus_n_O in H; rewrite > H; clear H; rewrite > mod_plus; - letin K ≝ (eq_nat_of_byte8_mod t); clearbody K; - letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool t1) 256 ?); clearbody K'; + letin K ≝ (eq_nat_of_byte8_mod a); clearbody K; + letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool b) 256 ?); clearbody K'; [ autobatch | ]; autobatch paramodulation. qed. -- 2.39.2