From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 19 May 2008 11:59:37 +0000 (+0000)
Subject: Dummy dependent types are no longer cleaned in inductive type arities.
X-Git-Tag: make_still_working~5147
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bbb941eb47625a07d36e0e45d6172cfa99bca027;p=helm.git

Dummy dependent types are no longer cleaned in inductive type arities.
---

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.