let _,_,t,_ = List.assoc n subst in
let hd = NCicSubstitution.subst_meta status lc t in
aux ctx
- (NCicReduction.head_beta_reduce (status :> NCic.status) ~upto:(List.length args)
+ (NCicReduction.head_beta_reduce (status :> NCicEnvironment.status) ~upto:(List.length args)
(match hd with
| NCic.Appl l -> NCic.Appl (l@args)
| _ -> NCic.Appl (hd :: args)))
let ppobj status obj = on_buffer (ppobj status) obj;;
+class type cstatus =
+ object
+ inherit NCicEnvironment.status
+ inherit NCic.cstatus
+ end
+
class status (uid : string option) =
object(self)
+ inherit NCicEnvironment.status uid
(* this method is meant to be overridden in ApplyTransformation *)
method user = uid
method ppterm = ppterm self