]> matita.cs.unibo.it Git - helm.git/commitdiff
removed some debugging prints
authorStefano Zacchiroli <zack@upsilon.cc>
Thu, 8 Sep 2005 12:49:43 +0000 (12:49 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Thu, 8 Sep 2005 12:49:43 +0000 (12:49 +0000)
helm/ocaml/tactics/reductionTactics.ml

index 8f806883eb580155b9405f6339ace37b524bce26..4abf2fb07a800427f75aae03d0aa1df7db2dbd46 100644 (file)
@@ -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