;;
let content2pres0
- ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
+ ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+ (term2pres : ?prec:int -> 'a)
(id,params,metasenv,obj)
=
match obj with
(TermContentPres.pp_ast ast)))
let ncontent2pres0
- ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
+ ?skip_initial_lambdas ?(skip_thm_and_qed=false)
+ (term2pres : ?prec:int -> 'a)
(id,params,metasenv,obj : CicNotationPt.term Content.cobj)
=
match obj with