From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 20 May 2006 10:11:47 +0000 (+0000)
Subject: removed a bad prerr_endline
X-Git-Tag: make_still_working~7347
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3895e3a39df0bf828355c93da02cd2854a0b31e1;p=helm.git

removed a bad prerr_endline
---

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 8a31d6253..c8e74642b 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/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"