X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdama%2Fordered_uniform.ma;h=6f72cd2449cf34b60ad1fc9619661ef5b1ed56fb;hb=34cdd4af2d7bdac3bab74a54123fbfcb02fa0403;hp=3485ae4c0e8bcb23efedc8475f561030ddea5918;hpb=f2bf34a07e2494d81ab7c3b44c143dec33e51fe8;p=helm.git

diff --git a/helm/software/matita/library/dama/ordered_uniform.ma b/helm/software/matita/library/dama/ordered_uniform.ma
index 3485ae4c0..6f72cd244 100644
--- a/helm/software/matita/library/dama/ordered_uniform.ma
+++ b/helm/software/matita/library/dama/ordered_uniform.ma
@@ -46,9 +46,9 @@ definition invert_os_relation ≝
   λC:ordered_set.λU:C squareO → Prop.
     λx:C squareO. U 〈\snd x,\fst x〉.
 
-interpretation "relation invertion" 'invert a = (invert_os_relation _ a).
-interpretation "relation invertion" 'invert_symbol = (invert_os_relation _).
-interpretation "relation invertion" 'invert_appl a x = (invert_os_relation _ a x).
+interpretation "relation invertion" 'invert a = (invert_os_relation ? a).
+interpretation "relation invertion" 'invert_symbol = (invert_os_relation ?).
+interpretation "relation invertion" 'invert_appl a x = (invert_os_relation ? a x).
 
 lemma hint_segment: ∀O.
  segment (Type_of_ordered_set O) →
@@ -210,7 +210,7 @@ intros (O s); apply mk_ordered_uniform_space;
 qed.
 
 interpretation "Ordered uniform space segment" 'segset a = 
- (segment_ordered_uniform_space _ a).
+ (segment_ordered_uniform_space ? a).
 
 (* Lemma 3.2 *)
 alias symbol "pi1" = "exT \fst".