debug pps removed

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 8edf316f695222e86dab1343fb360af59e46029d..4abfc933eb7b59b83b413d07c1128e4e92d3ea37 100644 (file)
--- 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 b80bfc5001f12aa41b0d9a5d2dfde04be9aee7ad..5f75fb3aa8b24b828a554455df0e0e04fbd4aa02 100644 (file)
--- 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 ffa2422e4afc21151992e7a5f3e8510ad20e19ad..6bcda0df86781d8abe3f61bc5334bed860a2b6e3 100644 (file)
--- 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