-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, string) Hashtbl.t ->
+ Cic.annterm Content.cobj -> Mpresentation.mpres