From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 17:55:16 +0000 (+0000)
Subject: Dummy dependent types are no longer cleaned in inductive type arities.
X-Git-Tag: make_still_working~5166
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b3f75a04f7516037a1c3dc0735ed17720663356c;hp=bba3b7f83610c3babb797e8ce1e844a560303295;p=helm.git

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

diff --git a/helm/software/matita/library/Z/dirichlet_product.ma b/helm/software/matita/library/Z/dirichlet_product.ma
index 6328bc7dc..c45b4dc53 100644
--- a/helm/software/matita/library/Z/dirichlet_product.ma
+++ b/helm/software/matita/library/Z/dirichlet_product.ma
@@ -257,7 +257,7 @@ apply (trans_eq ? ?
                        assumption
                       ]
                     |elim (divides_b_true_to_divides ? ? H4).
-                     apply (witness ? ? n2).
+                     apply (witness ? ? n1).
                      rewrite > assoc_times.
                      rewrite < H5.
                      rewrite < sym_times.
diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma
index 1765b3807..1bb493f79 100644
--- a/helm/software/matita/library/nat/chebyshev_teta.ma
+++ b/helm/software/matita/library/nat/chebyshev_teta.ma
@@ -162,7 +162,7 @@ elim (bc2 (S(2*m)) m)
   [unfold bc.rewrite > H3.
    rewrite > sym_times.
    rewrite > lt_O_to_div_times
-    [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n2)
+    [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n1)
       [apply False_ind.
        elim (divides_times_to_divides p (m!) (S (2*m)-m)!)
         [apply (lt_to_not_le ? ? (lt_to_le ? ? H1)).
diff --git a/helm/software/matita/library/nat/congruence.ma b/helm/software/matita/library/nat/congruence.ma
index 753745d45..948d10667 100644
--- a/helm/software/matita/library/nat/congruence.ma
+++ b/helm/software/matita/library/nat/congruence.ma
@@ -118,7 +118,7 @@ qed.
 theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to 
 divides p (n - m) \to congruent n m p.
 intros.elim H2.
-apply (eq_times_plus_to_congruent n m p n2).
+apply (eq_times_plus_to_congruent n m p n1).
 assumption.
 rewrite < sym_plus.
 apply minus_to_plus.assumption.
diff --git a/helm/software/matita/library/nat/gcd_properties1.ma b/helm/software/matita/library/nat/gcd_properties1.ma
index bb8b9bb53..776b38adf 100644
--- a/helm/software/matita/library/nat/gcd_properties1.ma
+++ b/helm/software/matita/library/nat/gcd_properties1.ma
@@ -25,7 +25,7 @@ c \divides a \to c \divides b \to
 intros.
 elim (H2 ((gcd a b)))
 [ apply (antisymmetric_divides (gcd a b) c)
-  [ apply (witness (gcd a b) c n2).
+  [ apply (witness (gcd a b) c n1).
     assumption
   | apply divides_d_gcd;
       assumption
@@ -164,7 +164,7 @@ apply (nat_case1 a)
           ]
         | assumption
         ]
-      | apply (witness ? ? n2).
+      | apply (witness ? ? n1).
         apply (inj_times_r1 (gcd a b) Hcut1).
         rewrite < assoc_times.
         rewrite < sym_times in \vdash (? ? (? % ?) ?).
@@ -328,13 +328,13 @@ apply gcd1
 | intros.
   elim H1.
   elim H2.
-  cut(b = (d*n2) + a) 
-  [ cut (b - (d*n2) = a)
+  cut(b = (d*n1) + a) 
+  [ cut (b - (d*n1) = a)
     [ rewrite > H4 in Hcut1.
-      rewrite < (distr_times_minus d n n2) in Hcut1.
+      rewrite < (distr_times_minus d n n1) in Hcut1.
       apply divides_d_gcd
       [ assumption
-      | apply (witness d a (n - n2)).
+      | apply (witness d a (n - n1)).
         apply sym_eq.
         assumption
       ]
diff --git a/helm/software/matita/library/nat/neper.ma b/helm/software/matita/library/nat/neper.ma
index 8da13d9ab..f5847033a 100644
--- a/helm/software/matita/library/nat/neper.ma
+++ b/helm/software/matita/library/nat/neper.ma
@@ -280,7 +280,7 @@ rewrite > lt_O_to_div_times
      assumption
     |apply lt_exp_Sn_n_SSSO
     ]
-  |apply (O_lt_times_to_O_lt ? n2).
+  |apply (O_lt_times_to_O_lt ? n1).
    rewrite < H2.
    assumption
   ]