Replaced long, bugged implementation of letin-tac with two lines of code :-)

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 5186345b661ad58a8355be382e3ca589cc1309ef..7937e8b4b4ddbb739ed6fb27bafa82a0b3f7f7ea 100644 (file)
--- 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;;