From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 Jul 2005 12:13:16 +0000 (+0000)
Subject: Cosmetic changes: a piece of code replaced with a pre-defined function.
X-Git-Tag: pre_notation~74
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=468e3b35a467e49edb8e5e83469d24520aff83ee;p=helm.git

Cosmetic changes: a piece of code replaced with a pre-defined function.
---

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index 7eae7fb5c..99bfd2081 100644
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -103,11 +103,9 @@ let rewrite_tac ~direction ~pattern equality =
       (PT.exact_tac ~term:exact_proof) ((curi,metasenv',pbo,pty),goal)
   in
   assert (List.length goals = 0) ;
-  let goals = List.map (fun (i,_,_) -> i) metasenv' in
   let goals =
-   List.filter
-    (fun i ->
-      not (List.exists (fun (j,_,_) -> i=j) metasenv)) goals
+   ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+    ~newmetasenv:metasenv'
   in
    (proof',goals)
  in