type mml_of_cic_sequent =
Cic.metasenv ->
int * Cic.context * Cic.term ->
- Gdome.document *
+ Gdome.document *
+ (Cic.annconjecture *
((Cic.id, Cic.term) Hashtbl.t *
(Cic.id, Cic.id option) Hashtbl.t *
- (string, Cic.hypothesis) Hashtbl.t)
+ (string, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t))
+
type mml_of_cic_object =
- explode_all:bool ->
- UriManager.uri ->
- Cic.annobj ->
- (string, string) Hashtbl.t ->
- (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
+ Cic.obj ->
+ Gdome.document *
+ (Cic.annobj *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (Cic.id, Cic.conjecture) Hashtbl.t *
+ (Cic.id, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t *
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t))
(** A widget to render sequents **)
?vadjustment:GData.adjustment ->
?font_size:int ->
?log_verbosity:int ->
- ?border_width:int ->
?width:int ->
?height:int ->
?packing:(GObj.widget -> unit) ->
(* load_proof also returns the annotated cic term and the *)
(* ids_to_inner_types and ids_to_inner_sorts maps. *)
method load_proof :
- UriManager.uri -> Cic.obj ->
+ Cic.obj ->
Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t *
(Cic.id, string) Hashtbl.t
?vadjustment:GData.adjustment ->
?font_size:int ->
?log_verbosity:int ->
- ?border_width:int ->
?width:int ->
?height:int ->
?packing:(GObj.widget -> unit) ->