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=99bcbbf050c1cac7c4bdd054fed79f40e047a434;hpb=c5a4db6c1020488d0792cee00dcf395a0ce54735;p=helm.git

diff --git a/helm/software/matita/library/dama/ordered_uniform.ma b/helm/software/matita/library/dama/ordered_uniform.ma
index 99bcbbf05..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) →
@@ -127,12 +127,12 @@ cases H;
         change in H1:(? ? ? %) with (\fst b); 
         change in a with (hos_carr (half_segment_ordered_set ? s));
         change in b with (hos_carr (half_segment_ordered_set ? s));
-        apply rule H1;
+        apply rule (x2sx_ ? s ?? H1);
 | right; change in H1:(? ? % ?) with (\fst b); 
         change in H1:(? ? ? %) with (\fst a); 
         change in a with (hos_carr (half_segment_ordered_set ? s));
         change in b with (hos_carr (half_segment_ordered_set ? s));
-        apply rule H1;]
+        apply rule (x2sx_ ? s ?? H1);]
 qed.
 
 
@@ -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".