X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=5c19f925e96c64794cf52c26185eaccafb941f5a;hb=c156170ba340354ea3da250b4d6c35d80c855849;hp=c440795ffc2a099ee041fbe8039bc5f20bf478f3;hpb=b396fcf2d604ed9b9952217539ff69e2f5fff3c5;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index c440795ff..5c19f925e 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -228,7 +228,7 @@ definition equality_morphism_of_symmetric_areflexive_transitive_relation:
     unfold transitive in H;
     unfold symmetric in sym;
     intro;
-    auto
+    auto new
   ].
 qed.
 
@@ -246,10 +246,11 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     intro;
     unfold transitive in H;
     unfold symmetric in sym;
-    auto.
+    auto depth=4.
   ]
 qed.
 
+(*
 definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
  ∀(A: Type)(Aeq: relation A)(trans: transitive ? Aeq).
   let ASetoidClass1 := AsymmetricAreflexive Contravariant Aeq in
@@ -257,7 +258,7 @@ definition equality_morphism_of_asymmetric_areflexive_transitive_relation:
    (Morphism_Theory (cons ASetoidClass1 (singl ASetoidClass2)) Impl_Relation_Class).
  intros.
  exists Aeq.
- unfold make_compatibility_goal; simpl; unfold impl; eauto.
+ unfold make_compatibility_goal; simpl; unfold impl; auto.
 qed.
 
 definition equality_morphism_of_asymmetric_reflexive_transitive_relation:
@@ -745,3 +746,4 @@ Ltac refl_st := match goal with
 definition gen_st : ∀A : Set. Setoid_Theory ? (@eq A).
 Proof. constructor; congruence. Qed.
 
+*)
\ No newline at end of file