From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Nov 2009 09:21:13 +0000 (+0000)
Subject: 1) sort computation undone (it used to be bugged anyway)
X-Git-Tag: make_still_working~3217
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8e1b4eb6c9c8544f754b525d6cf2ba5ab0bf5396;p=helm.git

1) sort computation undone (it used to be bugged anyway)
2) let's unfocus again (even if it is not always correct)
---

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index f5d29784a..640128616 100644
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1168,7 +1168,7 @@ let equational_and_applicative_case
                            let _, sort = typeof s (ctx_of gty) gty in
                            match term_of_cic_term s sort (ctx_of sort) with
                            | _, NCic.Sort NCic.Prop -> P
-                           | _ -> T
+                           | _ -> (*T*)P
                       in
                i,sort) gl) elems 
  in
@@ -1484,8 +1484,8 @@ let auto_main flags signature (pos : 'a and_pos) cache =
           if has_no_alternative then (L (g,status)) else (S (g,status))in
         (* TODO: cache success g *)
         let pos = if has_no_alternative then Z.inject T.Nil pos else pos in
-(*         let status = if unfocus then NTactics.unfocus_tac status else status
- *         in *)
+         let status = if unfocus then NTactics.unfocus_tac status else status
+         in
         let news = status,size,depth in
         let pos = Z.setA news newg pos in
         match Z.right pos with