From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 9 Apr 2009 09:47:05 +0000 (+0000)
Subject: minor fixes
X-Git-Tag: make_still_working~4100
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df9b1c00777e4ff1c73b467624bbc3117c1bb0a3;p=helm.git

minor fixes
---

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 58f86c89e..a2042dda6 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -156,13 +156,8 @@ let block_tac l status =
 let compare_statuses ~past ~present =
  let _,_,past,_,_ = past.pstatus in 
  let _,_,present,_,_ = present.pstatus in 
- let closed = 
-  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
- in
- let opened = 
-   List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present)
- in
- opened, closed
+ List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
+ List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
 ;;
 
 
@@ -308,11 +303,16 @@ let generalize_tac ~where =
  block_tac [ 
    select_tac ~where ~job:(`Collect l) true; 
    force (lazy (distribute_tac (fun status goal ->
+     if !l = [] then fail (lazy "No term to generalize");
      let goalty = get_goalty status goal in
-     (* unift (ctx_of goal) t s *)
+     let canon = List.hd !l in
+     let status = 
+       List.fold_left 
+         (fun s t -> unify s (ctx_of goalty) canon t) status (List.tl !l)
+     in
      instantiate status goal 
        (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; 
-         term_of_cic_term (List.hd !l) (ctx_of goalty) ]))
+         term_of_cic_term canon (ctx_of goalty) ]))
    ))) ]
 ;;