type lowtac_status = {
pstatus : NCic.obj;
- lstatus : LexiconEngine.status
+ estatus : NEstatus.status;
}
type lowtactic = lowtac_status -> int -> lowtac_status
val whd:
lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
lowtac_status * cic_term
+val normalize:
+ lowtac_status -> ?delta:int -> NCic.context -> cic_term ->
+ lowtac_status * cic_term
val typeof:
lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
val unify:
val apply_subst:
lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
-
val get_goalty: lowtac_status -> int -> cic_term
val mk_meta:
lowtac_status -> ?name:string -> NCic.context ->