From 5da97dd622a5f94dd8bc21ffb15b6b63ff078488 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 21:00:31 +0000 Subject: [PATCH] Dummy dependent types are no longer cleaned in inductive type arities. --- helm/software/matita/contribs/RELATIONAL/ZEq/setoid.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- 2.39.2