From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 5 Nov 2008 21:27:18 +0000 (+0000)
Subject: duplicate entry in menv avoided
X-Git-Tag: make_still_working~4599
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3a0c71609f757f4ad3aadd234b84486fec97b791;p=helm.git

duplicate entry in menv avoided
---

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index c8ab4e428..7cb9fb0e5 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1623,7 +1623,12 @@ let all_subsumed bag maxm status active passive =
                status goalproof newproof subsumption_id subsumption_subst proof_menv
 	   in
 	   let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
-	   let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
+           let newmetasenv = 
+             other_menv @ 
+             List.filter
+               (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
+           in
+	   let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
 	     (subst, proof,gl)) subsumed_or_id 
   in 
   res, !maxmeta