#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 ->