| Some j -> [j]
in
let index_term1, index_term2 =
- if (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
- || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down)
- then 2,5 else 5,2
+ if conclude.Con.conclude_method = "RewriteLR" then 2,5 else 5,2
in
let term1 =
(match List.nth conclude.Con.conclude_args index_term1 with
content2pres ?skip_initial_lambdas ?skip_thm_and_qed
(fun ?(prec=90) annterm ->
let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+ TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
in
CicNotationPres.box_of_mpres
(CicNotationPres.render ids_to_uris ~prec