From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 19 Dec 2008 12:44:13 +0000 (+0000)
Subject: fixed, it seems the new handling of hints in some rare cases made inference stupid
X-Git-Tag: make_still_working~4352
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f2bf34a07e2494d81ab7c3b44c143dec33e51fe8;p=helm.git

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 4f7a2f847..6dc55e142 100644
--- 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 99bcbbf05..3485ae4c0 100644
--- 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 26ffd59bc..e482d79a0 100644
--- 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;