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 7eae7fb5c0ee402d0761dd39df7fe4050d7ad4ce..99bfd2081c83e46c5c6426da02e0225a06611b65 100644 (file)
--- 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