From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 14 Jun 2006 14:30:32 +0000 (+0000)
Subject: removed old debugging print
X-Git-Tag: make_still_working~7192
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0c0bc425d6a4a765e084e91d2628db4c55e81c65;p=helm.git

removed old debugging print
---

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 2a7a3f2d0..e44c6b588 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -313,11 +313,6 @@ let is_prefix prefix string =
   else None
 
 let remove_prefix prefix (last,string) =
-  if prefix="append" then
-    begin 
-      prerr_endline last;
-      prerr_endline string;
-    end;
   if string = "" then (last,string)
   else 
     match is_prefix prefix string with
@@ -461,8 +456,6 @@ let rec check_names ctx hyp_names conclusion_name t =
 	hyp_names=[] && check_name ~allow_suffix:true ctx conclusion_name t
 
 let check name term =
-(*  prerr_endline name;
-  prerr_endline (ppterm term); *)
   let names = Str.split (Str.regexp_string "_to_") name in
   let hyp_names,conclusion_name =
     match List.rev names with