minor fixes

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 58f86c89eb4d1d1e42a75128062ece37fc5f0b25..a2042dda6d2ce6d40d491f2512f96b0714c61dea 100644 (file)
--- 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) ]))
    ))) ]
 ;;