From df9b1c00777e4ff1c73b467624bbc3117c1bb0a3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 9 Apr 2009 09:47:05 +0000 Subject: [PATCH] minor fixes --- .../software/components/ng_tactics/nTactics.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) 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) ])) ))) ] ;; -- 2.39.2