From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Apr 2008 10:16:00 +0000 (+0000)
Subject: added a simplify to prevent the generation of an ugly fix
X-Git-Tag: make_still_working~5367
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=60218a0347847f6797575c7fa33a98ac6862e6cf;p=helm.git

added a simplify to prevent the generation of an ugly fix
---

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index f9c5e878b..36bea989e 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -929,7 +929,7 @@ definition interp_relation_class_list :
      rewrite <
        (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
      exact c1
-  | split;
+  | simplify; split;
      [ rewrite <
         (about_carrier_of_relation_class_and_relation_class_of_argument_class S);
        exact c1