type state = P.state
let empty_state = P.empty_state
+let size_of_state = P.size_of_state
+
let forward_infer_step status metasenv subst context s t ty =
let bag = P.bag_of_state s in
let saturate (t,ty) =
NCicBlob.saturate status metasenv subst context t ty in
- let bag,clause = P.mk_passive bag (t,ty) in
+ let bag,clause = P.mk_passive bag (saturate (t,ty)) in
if Terms.is_eq_clause clause then
- P.forward_infer_step (P.replace_bag s bag) clause 0
- else (debug (lazy "not eq"); s)
+ ((*prerr_endline "is eq";*)
+ P.forward_infer_step (P.replace_bag s bag) clause 0)
+ else ((*print (lazy "not eq");*) s)
;;
let index_obj status s uri =
NCicMetaSubst.saturate status ~delta:0 metasenv subst context
ty 0
in match hty with
- | NCic.Appl (eq ::tl) when eq = CB.eqP -> true
+ | NCic.Appl (eq ::tl) when eq = CB.eqP() -> true
| _ -> false
;;