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 99bcbbf050c1cac7c4bdd054fed79f40e047a434..3485ae4c0e8bcb23efedc8475f561030ddea5918 100644 (file)
--- a/helm/software/matita/library/dama/ordered_uniform.ma
+++ b/helm/software/matita/library/dama/ordered_uniform.ma
@@ -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.