From de9926defa9fdb4aaebbad4f4131b7704602597b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 16 Apr 2009 13:55:36 +0000 Subject: [PATCH] Replaced long, bugged implementation of letin-tac with two lines of code :-) --- .../components/ng_tactics/nTactics.ml | 22 +++++-------------- 1 file changed, 5 insertions(+), 17 deletions(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 5186345b6..7937e8b4b 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -370,23 +370,11 @@ let change_tac ~where ~with_what = select0_tac ~where ~job:(`ChangeWith change) ;; -let letin_tac ~where:(_,_,(m,hyp,gp)) ~what:(_,_,w) name = - assert(m = None); - let where = Some w, [], - match gp with - | None -> Some Ast.Implicit - | Some where -> - Some - (List.fold_left - (fun t _ -> - Ast.Binder(`Pi,(Ast.Ident("_",None),Some Ast.UserInput),t)) - where hyp) - in - block_tac [ - generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyp); - exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit)); - change_tac ~where:("",0,where) ~with_what:("",0,Ast.Ident (name,None)) - ] +let letin_tac ~where ~what:(_,_,w) name = + block_tac [ + select_tac ~where ~job:(`Substexpand 1) true; + exact_tac ("",0,Ast.LetIn((Ast.Ident (name,None),None),w,Ast.Implicit)); + ] ;; let apply_tac = exact_tac;; -- 2.39.2