From 97d5c628470f472501ee41a5cc2e045ca89bfbf0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 20 May 2006 10:11:47 +0000 Subject: [PATCH] removed a bad prerr_endline --- components/tactics/paramodulation/saturation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 8a31d6253..c8e74642b 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -1837,7 +1837,7 @@ let saturate proof goalno (CicMetaSubst.apply_subst final_subst) real_menv in let open_goals = - match free_meta with Some (Cic.Meta (m,_)) -> [m] | _ -> [] + match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] in Printf.eprintf "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" -- 2.39.2