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 f5d29784ae3a46294eb67b2f50e8c9b28cc9345a..640128616719fdbeb76aa7eead5beed334e15e40 100644 (file)
--- 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