X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fformal_topology%2Foverlap%2Fr-o-basic_pairs.ma;h=310ef55ebf53f23dbd552cda169685204ec5b17b;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=a50ed8cc26a5d505876a9c48ca7ebf76f1417145;hpb=ddc0a7b3f0acd57f879e540e696f69ca0c20bbf5;p=helm.git

diff --git a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
index a50ed8cc2..310ef55eb 100644
--- a/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/r-o-basic_pairs.ma
@@ -94,7 +94,7 @@ lemma curry: ∀A,B,C.binary_morphism1 A B C → A → B ⇒ C.
 qed.
 
 notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
-interpretation "map arrows 2" 'map_arrows F x = (fun12 _ _ (map_arrows2 _ _ F _ _) x).
+interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
 
 definition preserve_sup : ∀S,T.∀ f:Ω \sup S ⇒ Ω \sup T. CProp1.
 intros (S T f); apply (∀X:Ω \sup S. (f X) = ?);