(* *)
(**************************************************************************)
-val proof2pres :
- ('a -> Mpresentation.mpres) ->
- 'a Cic2content.proof ->
- Mpresentation.mpres
-
-(* val content2pres : Cic.annterm Cic2content.proof -> Mpresentation.mpres *)
-
-
-
-
-
+val content2pres:
+ ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
+ Cic.annterm Content.cobj ->
+ unit Mpresentation.mpres Box.box