let compare x y =
(* CSC: NCicPp.status is the best I can put here *)
- if NCicReduction.alpha_eq (new NCicPp.status) [] [] [] x y then 0
+ (* WR: and I can't guess a user id, so I must put None *)
+ if NCicReduction.alpha_eq (new NCicPp.status None) [] [] [] x y then 0
(* if x = y then 0 *)
else compare x y
;;
let pp t =
(* CSC: NCicPp.status is the best I can put here *)
- (new NCicPp.status)#ppterm ~context:C.context
+ (* WR: and I can't guess a user id, so I must put None *)
+ (new NCicPp.status None)#ppterm ~context:C.context
~metasenv:C.metasenv ~subst:C.subst t;;
type input = NCic.term
let saturate t ty =
let sty, _, args =
(* CSC: NCicPp.status is the best I can put here *)
- NCicMetaSubst.saturate (new NCicPp.status) ~delta:0 C.metasenv C.subst
+ (* WR: and I can't guess a user id, so I must put None *)
+ NCicMetaSubst.saturate (new NCicPp.status None) ~delta:0 C.metasenv C.subst
C.context ty 0
in
let proof =