From f2bf34a07e2494d81ab7c3b44c143dec33e51fe8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Dec 2008 12:44:13 +0000 Subject: [PATCH] fixed, it seems the new handling of hints in some rare cases made inference stupid --- .../library/dama/models/increasing_supremum_stabilizes.ma | 2 +- helm/software/matita/library/dama/ordered_uniform.ma | 4 ++-- helm/software/matita/library/dama/property_sigma.ma | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) 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; -- 2.39.2