X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=f9916befc851b48a2eeca70d6aa7d476fc819740;hb=a3ee89dab26307ce1cedc8041ede995a97d51446;hp=5186345b661ad58a8355be382e3ca589cc1309ef;hpb=13049dd275c7cb45b003f5860f1a400a66e37b06;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 5186345b6..f9916befc 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -336,25 +336,37 @@ let generalize_tac ~where =
    select_tac ~where ~job:(`Collect l) true; 
    print_tac true "ha selezionato?";
    (fun s -> distribute_tac (fun status goal ->
-     if !l = [] then fail (lazy "No term to generalize");
-     let goalty = get_goalty status goal in
-     let canon = List.hd !l in
-     let status = 
+      let goalty = get_goalty status goal in
+      let status,canon,rest =
+       match !l with
+          [] ->
+           (match where with
+               _,_,(None,_,_)  -> fail (lazy "No term to generalize")
+             | txt,txtlen,(Some what,_,_) ->
+                let status, what =
+                 disambiguate status (txt,txtlen,what) None (ctx_of goalty)
+                in
+                 status,what,[]
+           )
+        | he::tl -> status,he,tl in
+      let status = 
        List.fold_left 
-         (fun s t -> unify s (ctx_of goalty) canon t) status (List.tl !l)
-     in
-     let status, canon = term_of_cic_term status canon (ctx_of goalty) in
-     instantiate status goal 
-      (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
+         (fun s t -> unify s (ctx_of goalty) canon t) status rest in
+      let status, canon = term_of_cic_term status canon (ctx_of goalty) in
+      instantiate status goal 
+       (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ]))
    ) s) ]
 ;;
 
-let eval_tac ~reduction ~where =
+let reduce_tac ~reduction ~where =
   let change status t = 
     match reduction with
+    | `Normalize perform_delta ->
+        normalize status
+         ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
     | `Whd perform_delta -> 
-         whd status
-           ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
+        whd status
+         ?delta:(if perform_delta then None else Some max_int) (ctx_of t) t
   in
   let where = GrafiteDisambiguate.disambiguate_npattern where in
   select0_tac ~where ~job:(`ChangeWith change)
@@ -370,23 +382,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;;
@@ -553,3 +553,15 @@ let assert_tac seqs status =
           [merge_tac])
      ) status
 ;;
+
+let auto ~params status goal =
+  let gty = get_goalty status goal in
+  let n,h,metasenv,subst,o = status.pstatus in
+  let status,t = term_of_cic_term status gty (ctx_of gty) in
+    Paramod.nparamod metasenv subst (ctx_of gty) t;      
+    status
+;;
+
+let auto_tac ~params status =
+  distribute_tac (auto ~params) status
+;;