]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/reductionTactics.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / tactics / reductionTactics.ml
index 4abf2fb07a800427f75aae03d0aa1df7db2dbd46..4fc192a5b261f48be145c3e21cc7268c14a47055 100644 (file)
@@ -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)