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))
+
(* List utility functions *)
exception Skip;;
method load_sequent metasenv sequent =
(**** SIAM QUI ****)
- let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
+ let sequent_mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses,ids_to_inner_sorts)) =
mml_of_cic_sequent metasenv sequent
in
self#load_root ~root:sequent_mml#get_documentElement ;
end
| None -> assert false (* "ERROR: No selection!!!" *)
- method load_proof uri currentproof =
- let
- (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
- ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
- = Cic2acic.acic_object_of_cic_object currentproof
- in
- let mml =
- mml_of_cic_object
- ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+ method load_proof currentproof =
+ let mml,
+ (acic,
+ (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+ ids_to_hypotheses,ids_to_inner_sorts,ids_to_inner_types)) =
+ mml_of_cic_object currentproof
in
current_infos <-
Some