X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=4fc192a5b261f48be145c3e21cc7268c14a47055;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4abf2fb07a800427f75aae03d0aa1df7db2dbd46;hpb=ef7c83bce91f9077c5eafee157aac497095b6b88;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 4abf2fb07..4fc192a5b 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -191,12 +191,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)