From df9b1c00777e4ff1c73b467624bbc3117c1bb0a3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
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