X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicParamod.ml;h=fad1aa41157a96cdaf31669b598ca246601dfe78;hb=b0f18f8992623be7c7dde1890d51c7404e9930ab;hp=c680e8417346885453b2e70852d814065c6e0ed8;hpb=fa01419bafd483b5a043a93a2f812a98cf178e22;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index c680e8417..fad1aa411 100644
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -77,7 +77,7 @@ let nparamod rdb metasenv subst context t table =
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
   in
   let (bag,maxvar), passives = 
-    HExtlib.list_mapi_acc (fun x _ a -> prerr_endline "there"; P.mk_passive a x) (bag,maxvar) table
+    HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
   in
   match 
     P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
@@ -102,7 +102,6 @@ let empty_state = P.empty_state
 
 let forward_infer_step s t ty =
   let bag = P.bag_of_state s in
-  prerr_endline "here"; 
   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
@@ -112,8 +111,9 @@ let forward_infer_step s t ty =
 let index_obj s uri =
   let obj = NCicEnvironment.get_checked_obj uri in
   match obj with
-    | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
-	forward_infer_step s t ty
+    | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) ->
+        let nref = NReference.reference_of_spec uri (NReference.Def d) in
+	forward_infer_step s (NCic.Const nref) ty
     | _ -> s
 ;;