From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 11 Feb 2010 10:34:32 +0000 (+0000)
Subject: minimal sequent height set to 1
X-Git-Tag: make_still_working~3045
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=825fcd9784570617b610d7cb0308984a19f7ba87;p=helm.git

minimal sequent height set to 1
---

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 0d8655f54..e6010808b 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1448,7 +1448,7 @@ let fast_height_of_term t =
 let height_of_goals status = 
   let open_goals = head_goals status#stack in
   assert (List.length open_goals > 0);
-  let h = ref 0 in
+  let h = ref 1 in
   List.iter 
     (fun open_goal ->
       let ty = get_goalty status open_goal in
diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma
index 393f16189..a163960f7 100644
--- a/helm/software/matita/nlibrary/arithmetics/nat.ma
+++ b/helm/software/matita/nlibrary/arithmetics/nat.ma
@@ -840,7 +840,7 @@ ntheorem minus_Sn_m: ∀m,n:nat. m ≤ n → S n -m = S (n-m).
 #n; #m; #lenm; nelim lenm; napplyS refl_eq. *)
 napply nat_elim2; 
   ##[//
-  ##|#n; #abs; napply False_ind; (* XXX *) napply not_le_Sn_O; /2/.
+  ##|#n; #abs; napply False_ind; /2/.
   ##|#n; #m; #Hind; #c; napplyS Hind; /2/;
   ##]
 nqed.
@@ -859,7 +859,7 @@ ntheorem plus_minus:
 ∀m,n,p:nat. m ≤ n → (n-m)+p = (n+p)-m.
 napply nat_elim2; 
   ##[//
-  ##|#n; #p; #abs; napply False_ind; (* XXX *) napply not_le_Sn_O; /2/;
+  ##|#n; #p; #abs; napply False_ind; /2/;
   ##|nnormalize;/3/;
   ##]
 nqed.
@@ -1031,9 +1031,9 @@ ntheorem eqb_elim : ∀ n,m:nat.∀ P:bool → Prop.
 (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). 
 napply nat_elim2; 
   ##[#n; ncases n; nnormalize; /3/; 
-  ##|nnormalize; (* XXX *) nletin hint ≝ not_eq_O_S; /3/; 
+  ##|nnormalize; /3/; 
   ##|nnormalize; /4/; 
-  ##] (* XXX rimane aperto *) #m; #P; #_; #H; napply H; napply not_eq_O_S.
+  ##] 
 nqed.
 
 ntheorem eqb_n_n: ∀n. eqb n n = true.
@@ -1042,7 +1042,7 @@ nqed.
 
 ntheorem eqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m.
 #n; #m; napply (eqb_elim n m);//;
-#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/;
+#_; #abs; napply False_ind; /2/;
 nqed.
 
 ntheorem eqb_false_to_not_eq: ∀n,m:nat. eqb n m = false → n ≠ m.
@@ -1072,7 +1072,7 @@ ntheorem leb_elim: ∀n,m:nat. ∀P:bool → Prop.
 (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m).
 napply nat_elim2; nnormalize;
   ##[/2/
-  ##| (* XXX *) nletin hint ≝ not_le_Sn_O; /3/;
+  ##| /3/;
   ##|#n; #m; #Hind; #P; #Pt; #Pf; napply Hind;
     ##[#lenm; napply Pt; napply le_S_S;//;
     ##|#nlenm; napply Pf; #leSS; /3/;
@@ -1083,14 +1083,14 @@ nqed.
 ntheorem leb_true_to_le:∀n,m.leb n m = true → n ≤ m.
 #n; #m; napply leb_elim;
   ##[//;
-  ##|#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/;
+  ##|#_; #abs; napply False_ind; /2/;
   ##]
 nqed.
 
 ntheorem leb_false_to_not_le:∀n,m.
   leb n m = false → n ≰ m.
 #n; #m; napply leb_elim;
-  ##[#_; #abs; napply False_ind; (* XXX *) nletin hint ≝ not_eq_true_false; /2/;
+  ##[#_; #abs; napply False_ind; /2/;
   ##|/2/;
   ##]
 nqed.