(** {2 State handling} *)
-type id = string
-
val hide_coercions: bool ref
type db
method interp_db: db
end
-class status :
+class virtual status :
object ('self)
+ inherit g_status
inherit NCicCoercion.status
- method interp_db: db
method set_interp_db: db -> 'self
method set_interp_status: #g_status -> 'self
end
-type cic_id = string
-
val add_interpretation:
#status as 'status ->
string -> (* id / description *)
(string * 'term) list -> NotationPt.cic_appl_pattern ->
'term
+val nmap_term:
+ #status ->
+ metasenv:NCic.metasenv -> subst:NCic.substitution -> context:NCic.context ->
+ NCic.term ->
+ NotationPt.term *
+ (Content.id, NReference.reference) Hashtbl.t (* id -> reference *)
+
+val nmap_context:
+ #status ->
+ metasenv:NCic.metasenv -> subst:NCic.substitution ->
+ NCic.context ->
+ NotationPt.term Content.context *
+ (Content.id, NReference.reference) Hashtbl.t (* id -> reference *)
+
val nmap_sequent:
#status -> metasenv:NCic.metasenv -> subst:NCic.substitution ->
int * NCic.conjecture ->
NotationPt.term Content.conjecture *
- (id, NReference.reference) Hashtbl.t (* id -> reference *)
+ (Content.id, NReference.reference) Hashtbl.t (* id -> reference *)
val nmap_obj:
#status -> NCic.obj ->
NotationPt.term Content.cobj *
- (id, NReference.reference) Hashtbl.t (* id -> reference *)
+ (Content.id, NReference.reference) Hashtbl.t (* id -> reference *)