From 60218a0347847f6797575c7fa33a98ac6862e6cf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 10:16:00 +0000 Subject: [PATCH] added a simplify to prevent the generation of an ugly fix --- helm/software/matita/library/technicalities/setoids.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2