removed no longer used METAs

[helm.git] / helm / ocaml / tactics / reductionTactics.ml

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 4abf2fb07a800427f75aae03d0aa1df7db2dbd46..115faa80b65a58c88256f0f7cb8d05e8d903002d 100644 (file)
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 open ProofEngineTypes
 
 (* Note: this code is almost identical to change_tac and
@@ -191,12 +193,13 @@ let change_tac ~pattern with_what  =
            (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
        | _,_ -> assert false
     ) context selected_context ([], metasenv, ugraph) in
- let metasenv' = 
-   List.map (function 
-     | (n,_,_) when n = metano -> (metano,context',ty')
-     | _ as t -> t
-   ) metasenv
- in
+  let metasenv' = 
+    List.map
+      (function 
+        | (n,_,_) when n = metano -> (metano,context',ty')
+        | _ as t -> t)
+      metasenv
+  in
   (curi,metasenv',pbo,pty), [metano]
   in
     mk_tactic (change_tac ~pattern ~with_what)