fixed, it seems the new handling of hints in some rare cases made inference stupid

diff --git a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
index 4f7a2f847469050911a9861814792068f59e4cfe..6dc55e1426ae332f77ad84c4c88542d70cf150ec 100644 (file)
--- a/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
+++ b/helm/software/matita/library/dama/models/increasing_supremum_stabilizes.ma
@@ -119,7 +119,7 @@ exists [apply w]; intros; change with (x = \fst (a j));
 rewrite > (H4 ?); [2: reflexivity]
 apply le_to_le_to_eq;
 [1: apply os_le_to_nat_le;
-    apply (trans_increasing ? H ? ? (nat_le_to_os_le ?? H5));
+    apply (trans_increasing a H ? ? (nat_le_to_os_le ?? H5));
 |2: apply (trans_le ? x ?);[apply os_le_to_nat_le; apply (H2 j);]
     rewrite < (H4 ?); [2: reflexivity] apply le_n;]
 qed.

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.
 
 

diff --git a/helm/software/matita/library/dama/property_sigma.ma b/helm/software/matita/library/dama/property_sigma.ma
index 26ffd59bc38d366e802f98f48a57150b60793448..e482d79a05985db6cf3cb766698efeb763dbaa01 100644 (file)
--- a/helm/software/matita/library/dama/property_sigma.ma
+++ b/helm/software/matita/library/dama/property_sigma.ma
@@ -108,7 +108,7 @@ lapply (H9 ?? H10) as H11; [
   |7:apply (ge_reflexive (l : hos_carr (os_r C)));
   |8:apply (H12 i);
   |6:change with (a i ≤ a (m O));
-     apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]  
+     apply (trans_decreasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]  
 clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
 generalize in match (refl_eq nat (m p)); 
 generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;