end
class virtual status :
+ string option ->
object ('self)
inherit g_status
inherit NCicCoercion.status
#status ->
metasenv:NCic.metasenv -> subst:NCic.substitution -> context:NCic.context ->
NCic.term ->
- NotationPt.term *
- (Content.id, NReference.reference) Hashtbl.t (* id -> reference *)
+ NotationPt.term
val nmap_context:
#status ->
metasenv:NCic.metasenv -> subst:NCic.substitution ->
- NCic.context ->
- NotationPt.term Content.context *
- (Content.id, NReference.reference) Hashtbl.t (* id -> reference *)
+ NCic.context -> NotationPt.context
val nmap_sequent:
#status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
int * NCic.conjecture ->
- NotationPt.term Content.conjecture *
- (Content.id, NReference.reference) Hashtbl.t (* id -> reference *)
+ NotationPt.sequent
val nmap_obj:
- #status -> NCic.obj ->
- NotationPt.term Content.cobj *
- (Content.id, NReference.reference) Hashtbl.t (* id -> reference *)
+ #status -> NCic.obj -> NotationPt.term NotationPt.obj