;;
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
?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts
=
content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
+(* FG: prec not optional in my patch *)
(fun ?(prec=90) annterm ->
let ast, ids_to_uris =
TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
(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