From: Enrico Tassi 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