From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 18 Jun 2009 17:26:41 +0000 (+0000)
Subject: debug pps removed
X-Git-Tag: make_still_working~3843
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c18631e6e9aad36446af0c126e8616272f44a08a;p=helm.git

debug pps removed
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 8edf316f6..4abfc933e 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -975,7 +975,6 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
               subst_metasenv_and_fix_names nstatus)
             nstatus tacl
          in
-         NTacStatus.pp_tac_status nstatus;
          { status with GrafiteTypes.ng_status= GrafiteTypes.ProofMode nstatus },
          `New [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index b80bfc500..5f75fb3aa 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -192,11 +192,11 @@ let nparamod rdb metasenv subst context t table =
         let gsteps = List.rev gsteps in
         esteps@(i::gsteps)
       in
-      prerr_endline "YES!";
-      prerr_endline ("Meeting point : " ^ (string_of_int i));
+(*
       prerr_endline "Proof:"; 
       List.iter (fun x -> prerr_endline (string_of_int x);
               prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
+*)
       let proofterm = B.mk_proof bag i l in
       let metasenv, proofterm = 
         let rec aux k metasenv = function
@@ -209,15 +209,11 @@ let nparamod rdb metasenv subst context t table =
         in
          aux 0 metasenv proofterm
       in
-      prerr_endline
-        ("prova generata: " ^ NCicPp.ppterm 
-           ~metasenv ~subst ~context proofterm);
       let metasenv, subst, proofterm, _prooftype = 
         NCicRefiner.typeof 
           (rdb#set_coerc_db NCicCoercion.empty_db) 
           metasenv subst context proofterm None
       in
-      prerr_endline "prova raffinata";
       proofterm, metasenv, subst
   | Failure _ -> prerr_endline "FAILURE"; assert false
 ;;
diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index ffa2422e4..6bcda0df8 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -558,7 +558,6 @@ let undebruijnate inductive ref t rev_fl =
 let typeof_obj 
   rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
 = 
-prerr_endline ("===============\n" ^ NCicPp.ppobj (uri,height,metasenv,subst,obj));
   let check_type metasenv subst context (ty as orig_ty) =  (* XXX fattorizza *)
     let metasenv, subst, ty, sort = 
       typeof rdb ~localise metasenv subst context ty None