?history_size:int -> (** default 20 *)
?uri:UriManager.uri ->
typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+ attrs:Cic.attribute list ->
(proof_status -> 'a) -> (* init data *)
(proof_status * 'a -> proof_status -> 'a) -> (* update data *)
unit ->
method metasenv: Cic.metasenv
method body: Cic.term
method typ: Cic.term
+ method attrs: Cic.attribute list
(** change metasenv _without_ triggering any notification *)
method set_metasenv: Cic.metasenv -> unit
val trivial_status:
?uri:UriManager.uri ->
typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
+ attrs:Cic.attribute list ->
unit ->
unit status