From 1238c59b078908f3923aa2e03adee7fe7a291027 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Jun 2006 16:47:15 +0000 Subject: [PATCH] fixed generation of letins --- .../tactics/paramodulation/equality.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml index 6b3a1e0ef..5a8e88638 100644 --- a/helm/software/components/tactics/paramodulation/equality.ml +++ b/helm/software/components/tactics/paramodulation/equality.ml @@ -463,9 +463,10 @@ let build_proof_step eq lift subst p1 p2 pos l r pred = ;; let parametrize_proof p l r ty = - let parameters = - CicUtil.metas_of_term p @ CicUtil.metas_of_term l @ CicUtil.metas_of_term r - in (* ?if they are under a lambda? *) + let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in + let mot = CicUtil.metas_of_term_set in + let parameters = uniq (mot p @ mot l @ mot r) in + (* ?if they are under a lambda? *) let parameters = HExtlib.list_uniq (List.sort Pervasives.compare parameters) in @@ -578,9 +579,12 @@ let rec find_deps m i = let topological_sort l = (* build the partial order relation *) - let m = - List.fold_left (fun m i -> find_deps m i) - M.empty l + let m = List.fold_left (fun m i -> find_deps m i) M.empty l in + let m = (* keep only deps inside l *) + List.fold_left + (fun m' i -> + M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m') + M.empty l in let m = M.map (fun x -> Some x) m in (* utils *) @@ -601,7 +605,8 @@ let topological_sort l = let res = ok @ res in if ok = [] then res else aux m res in - aux m [] + let rc = List.rev (aux m []) in + rc ;; -- 2.39.2