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)))
| `Elim _sort -> "Elim _"
| `Projection -> "Projection"
| `InversionPrinciple -> "InversionPrinciple"
+ | `DiscriminationPrinciple -> "DiscriminationPrinciple"
| `Variant -> "Variant"
| `Local -> "Local"
| `Regular -> "Regular"
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