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

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index 8f806883e..4fc192a5b 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -137,11 +137,6 @@ let change_tac ~pattern with_what  =
     let pairs, metasenv, ugraph =
       List.fold_left
         (fun (pairs, metasenv, ugraph) (context_of_t, t) ->
-prerr_endline "++++++++++++++++++++++++++";
-prerr_endline "context_of_t";
-prerr_endline (CicMetaSubst.ppcontext [] context_of_t);
-prerr_endline "t";
-prerr_endline (CicMetaSubst.ppterm [] t);
           let with_what, metasenv, ugraph =
             with_what context_of_t metasenv ugraph
           in
@@ -196,12 +191,13 @@ prerr_endline (CicMetaSubst.ppterm [] t);
            (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)