...

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / basic_pairs_to_o-basic_pairs.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
index 3e2fe8f354ee116ad0e851d568893eaa14182b2a..65709f4650c13c3941af2ebde7f700a24935f8d3 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/basic_pairs_to_o-basic_pairs.ma
@@ -16,7 +16,6 @@ include "basic_pairs.ma".
 include "o-basic_pairs.ma".
 include "relations_to_o-algebra.ma".
 
-(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
 definition o_basic_pair_of_basic_pair: basic_pair → Obasic_pair.
  intro b;
  constructor 1;