Renaming.

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma
index 576fa5ea157b672268e8f25ac2ae3c9d2df7cca1..5a98136bc889dc6ef7b5e8ee246580cf9078cab4 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_basic_topologies.ma
@@ -23,11 +23,11 @@ definition basic_topology_of_basic_pair: basic_pair → basic_topology.
  letin obt ≝ (o_basic_topology_of_o_basic_pair obp);
  constructor 1;
   [ apply (form bp);
-  | apply (A obt);
-  | apply (J obt);
-  | apply (A_is_saturation obt);
-  | apply (J_is_reduction obt);
-  | apply (compatibility obt); ]
+  | apply (oA obt);
+  | apply (oJ obt);
+  | apply (oA_is_saturation obt);
+  | apply (oJ_is_reduction obt);
+  | apply (Ocompatibility obt); ]
 qed.
 
 definition continuous_relation_of_relation_pair:
@@ -38,6 +38,6 @@ definition continuous_relation_of_relation_pair:
  letin ocr ≝ (o_continuous_relation_of_o_relation_pair ?? orp);
  constructor 1;
   [ apply (rp \sub \f);
-  | apply (reduced ?? ocr);
-  | apply (saturated ?? ocr); ]
+  | apply (Oreduced ?? ocr);
+  | apply (Osaturated ?? ocr); ]
 qed.
\ No newline at end of file