From 8e1b4eb6c9c8544f754b525d6cf2ba5ab0bf5396 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Nov 2009 09:21:13 +0000 Subject: [PATCH] 1) sort computation undone (it used to be bugged anyway) 2) let's unfocus again (even if it is not always correct) --- helm/software/components/ng_tactics/nAuto.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 -- 2.39.2