From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 12 Jun 2008 08:40:06 +0000 (+0000)
Subject: fixed some regressions
X-Git-Tag: make_still_working~5037
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=99f153e43f18bc682339bed41c8230af2ac6fd2f;p=helm.git

fixed some regressions
---

diff --git a/helm/software/matita/contribs/dama/dama/lebesgue.ma b/helm/software/matita/contribs/dama/dama/lebesgue.ma
index bab1e26fa..46fe6e422 100644
--- a/helm/software/matita/contribs/dama/dama/lebesgue.ma
+++ b/helm/software/matita/contribs/dama/dama/lebesgue.ma
@@ -76,10 +76,10 @@ split;
     [1: intro j; cases (Hxy j); cases H3; cases H4; split;
         [apply (H5 0);|apply (H7 0)]
     |2: cases (H l u Xi X) (Ux Uy); apply Ux; cases Hx; split; [apply H3;]
-        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
         exists [apply w] apply H7; 
     |3: cases (H l u Yi X) (Ux Uy); apply Uy; cases Hy; split; [apply H3;]
-        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y) Hy);
+        cases H4; split; [apply H5] intros (y Hy);cases (H6 (fst y));[2:apply Hy];
         exists [apply w] apply H7;]]
 qed.
  
diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
index cf3a5b057..44be29543 100644
--- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
+++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma
@@ -37,7 +37,7 @@ lemma segment_preserves_uparrow:
     (λn.fst (a n)) ↑ x → a ↑ (sig_in ?? x h).
 intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
 split; [apply H1] intros;
-cases (H2 (fst y) H3); exists [apply w] assumption;
+cases (H2 (fst y)); [2: apply H3;] exists [apply w] assumption;
 qed.
 
 lemma segment_preserves_downarrow:
@@ -45,7 +45,7 @@ lemma segment_preserves_downarrow:
     (λn.fst (a n)) ↓ x → a ↓ (sig_in ?? x h).
 intros; cases H (Ha Hx); split [apply Ha] cases Hx; 
 split; [apply H1] intros;
-cases (H2 (fst y) H3); exists [apply w] assumption;
+cases (H2 (fst y));[2:apply H3]; exists [apply w] assumption;
 qed.
     
 (* Fact 2.18 *)
@@ -54,6 +54,7 @@ lemma segment_cauchy:
     a is_cauchy → (λn:nat.fst (a n)) is_cauchy.
 intros 7; 
 alias symbol "pi1" (instance 3) = "pair pi1".
+alias symbol "pi2" = "pair pi2".
 apply (H (λx:{[l,u]} square.U 〈fst (fst x),fst (snd x)〉));
 (unfold segment_ordered_uniform_space; simplify);
 exists [apply U] split; [assumption;]