many changes regarding coercions:

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / o-basic_topologies.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
index 873a9df60988a632084b8c6f24e9c2b00b619590..68b9befb82dd93e3e5acb5e4d4fd0feefc9b0b3a 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/o-basic_topologies.ma
@@ -116,9 +116,9 @@ definition continuous_relation_comp:
  intros (o1 o2 o3 r s); constructor 1;
   [ apply (s ∘ r);
   | intros;
-    apply sym1;
+    apply sym1; 
     change in match ((s ∘ r) U) with (s (r U));
-    (*<BAD>*) unfold FunClass_1_OF_Type_OF_setoid2;
+    (*<BAD>*) unfold FunClass_1_OF_Type_OF_setoid21;
     unfold objs2_OF_basic_topology1; unfold hint;
     letin reduced := reduced; clearbody reduced;
     unfold uncurry_arrows in reduced ⊢ %; (*</BAD>*)