freescale porting

[helm.git] / helm / software / matita / library / dama / ordered_uniform.ma

diff --git a/helm/software/matita/library/dama/ordered_uniform.ma b/helm/software/matita/library/dama/ordered_uniform.ma
index 5a712f127fa5eee5cd7ddf5e4540961cffb9207e..6f72cd2449cf34b60ad1fc9619661ef5b1ed56fb 100644 (file)
--- a/helm/software/matita/library/dama/ordered_uniform.ma
+++ b/helm/software/matita/library/dama/ordered_uniform.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "uniform.ma".
+include "dama/uniform.ma".
 
 record ordered_uniform_space_ : Type ≝ {
   ous_os:> ordered_set;
@@ -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".