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)
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
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
;;