(* *)
(******************************************************************************)
-(* Not exported:
-val apply_proof_stylesheets :
- Gdome.document -> explode_all:bool -> Gdome.document
-*)
-val apply_sequent_stylesheets : Gdome.document -> Gdome.document
-
-val mml_of_cic_term :
- int -> Cic.term ->
+val mml_of_cic_sequent :
+ Cic.metasenv ->
+ int * Cic.context * Cic.term ->
Gdome.document *
- (Cic.term * (Cic.id, Cic.term) Hashtbl.t *
- (Cic.id, Cic.id option) Hashtbl.t * (string, Cic.hypothesis) Hashtbl.t)
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (string, Cic.hypothesis) Hashtbl.t)
val mml_of_cic_object :
explode_all:bool ->