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

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

diff --git a/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
index 587470bfc..a9c9d0763 100644
--- a/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
+++ b/helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma
@@ -19,7 +19,7 @@ include "ZEq/defs.ma".
 
 theorem zeq_refl: \forall z. z = z.
  intros. elim z. clear z.
- lapply (nplus_total t t1). decompose.
+ lapply (nplus_total a b). decompose.
  autobatch.
 qed.