X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=bdf07fb8333f83d8fbecc3084a149d14d9bbc4f6;hb=fe5542c1ce4e78d2ec4e9b39cfc4f06182555e99;hp=b9abb44183389782a7e463eaeacf0801751010f5;hpb=fb6fee82bb9172e15b1a7bc7e20641627f593fcc;p=helm.git

diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml
index b9abb4418..bdf07fb83 100644
--- a/matita/components/content_pres/termContentPres.ml
+++ b/matita/components/content_pres/termContentPres.ml
@@ -575,7 +575,6 @@ let tail_names names env =
 
 let instantiate_level2 env term =
 (*   prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
-prerr_endline ("istanzio: " ^ NotationPp.pp_term term);
   let fresh_env = ref [] in
   let lookup_fresh_name n =
     try
@@ -585,9 +584,7 @@ prerr_endline ("istanzio: " ^ NotationPp.pp_term term);
       fresh_env := (n, new_name) :: !fresh_env;
       new_name
   in
-prerr_endline ("ENV " ^ NotationPp.pp_env env);
   let rec aux env term =
-prerr_endline ("istanzio_deep: " ^ NotationPp.pp_term term);
     match term with
     | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)