minor changes to make the library compile after wilmers new exists.

[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..3485ae4c0e8bcb23efedc8475f561030ddea5918 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;
@@ -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.