- let proof = proof2pres true term2pres ?skip_initial_lambdas p in
- if skip_thm_and_qed then
- proof
- else
- B.b_v
- [Some "helm","xref","id"]
- ([ B.b_h [] (B.b_kw ("theorem " ^ name) ::
- params2pres params @ [B.b_kw ":"]);
- B.H ([],[B.indent (term2pres thesis) ; B.b_kw "." ])] @
- metasenv2pres term2pres metasenv @
- [proof ; B.b_kw "qed."])
- | `Def (_, ty, `Definition body) ->
- let name = get_name body.Content.def_name in
- B.b_v
- [Some "helm","xref","id"]
- ([B.b_h []
- (B.b_kw ("definition " ^ name) :: params2pres params @ [B.b_kw ":"]);
- B.indent (term2pres ty)] @
- metasenv2pres term2pres metasenv @
- [B.b_kw ":=";
- B.indent (term2pres body.Content.def_term);
- B.b_kw "."])
- | `Decl (_, `Declaration decl)
- | `Decl (_, `Hypothesis decl) ->
- let name = get_name decl.Content.dec_name in
- B.b_v
- [Some "helm","xref","id"]
- ([B.b_h [] (B.b_kw ("axiom " ^ name) :: params2pres params);
- B.b_kw "Type:";
- B.indent (term2pres decl.Content.dec_type)] @
- metasenv2pres term2pres metasenv)
- | `Joint joint ->
- B.b_v []
- (recursion_kind2pres params joint.Content.joint_kind
- :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
- | _ -> raise ToDo
-
-let content2pres
- ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts
-=
- content2pres0 ?skip_initial_lambdas ?skip_thm_and_qed
- (fun ?(prec=90) annterm ->
- let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
- in
- CicNotationPres.box_of_mpres
- (CicNotationPres.render
- ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec
- (TermContentPres.pp_ast ast)))
-
-let ncontent2pres0
- ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres
- (id,params,metasenv,obj : CicNotationPt.term Content.cobj)
-=
- match obj with
- | `Def (Content.Const, thesis, `Proof p) ->
- let name = get_name p.Content.proof_name in
- let proof = proof2pres true term2pres ?skip_initial_lambdas p in