X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicParamod.ml;h=5b3e6148b99d4519ef0446941a35a10882a90f7a;hb=2371237a27b5fa23f741e381073a48d84bc6a906;hp=b3ab4d5047194c236b362460439cfbc79e21ad41;hpb=1cdd34d7c286ab22d942e2dd1b1420e1c1caeff6;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index b3ab4d504..5b3e6148b 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -107,11 +107,13 @@ let forward_infer_step s t ty = let bag,clause = P.mk_passive bag (t,ty) in if Terms.is_eq_clause clause then P.forward_infer_step (P.replace_bag s bag) clause 0 - else (prerr_endline "not eq"; s) + else (debug (lazy "not eq"); s) ;; let index_obj s uri = let obj = NCicEnvironment.get_checked_obj uri in + debug (lazy ("indexing : " ^ (NUri.string_of_uri uri))); + debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic uri))))); match obj with | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) -> let nref = NReference.reference_of_spec uri (NReference.Def d) in