1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (***************************************************************************)
30 (* Andrea Asperti <asperti@cs.unibo.it> *)
33 (***************************************************************************)
35 let p_mtr a b = Mpresentation.Mtr(a,b)
36 let p_mtd a b = Mpresentation.Mtd(a,b)
37 let p_mtable a b = Mpresentation.Mtable(a,b)
38 let p_mtext a b = Mpresentation.Mtext(a,b)
39 let p_mi a b = Mpresentation.Mi(a,b)
40 let p_mo a b = Mpresentation.Mo(a,b)
41 let p_mrow a b = Mpresentation.Mrow(a,b)
42 let p_mphantom a b = Mpresentation.Mphantom(a,b)
48 split (n-1) (List.tl l) in
53 let is_big_general countterm p =
54 let maxsize = Cexpr2pres.maxsize in
55 let module Con = Content in
56 let rec countp current_size p =
57 if current_size > maxsize then current_size
59 let c1 = (countcontext current_size p.Con.proof_context) in
60 if c1 > maxsize then c1
62 let c2 = (countapplycontext c1 p.Con.proof_apply_context) in
63 if c2 > maxsize then c2
65 countconclude c2 p.Con.proof_conclude
68 countcontext current_size c =
69 List.fold_left countcontextitem current_size c
71 countcontextitem current_size e =
72 if current_size > maxsize then maxsize
76 (match d.Con.dec_name with
77 Some s -> current_size + 4 + (String.length s)
78 | None -> prerr_endline "NO NAME!!"; assert false)
80 (match h.Con.dec_name with
81 Some s -> current_size + 4 + (String.length s)
82 | None -> prerr_endline "NO NAME!!"; assert false)
83 | `Proof p -> countp current_size p
85 (match d.Con.def_name with
87 let c1 = (current_size + 4 + (String.length s)) in
88 (countterm c1 d.Con.def_term)
90 prerr_endline "NO NAME!!"; assert false)
91 | `Joint ho -> maxsize + 1) (* we assume is big *)
93 countapplycontext current_size ac =
94 List.fold_left countp current_size ac
96 countconclude current_size co =
97 if current_size > maxsize then current_size
99 let c1 = countargs current_size co.Con.conclude_args in
100 if c1 > maxsize then c1
102 (match co.Con.conclude_conclusion with
103 Some concl -> countterm c1 concl
106 countargs current_size args =
107 List.fold_left countarg current_size args
109 countarg current_size arg =
110 if current_size > maxsize then current_size
113 Con.Aux _ -> current_size
114 | Con.Premise prem ->
115 (match prem.Con.premise_binder with
116 Some s -> current_size + (String.length s)
117 | None -> current_size + 7)
119 current_size + (String.length lemma.Con.lemma_name)
120 | Con.Term t -> countterm current_size t
121 | Con.ArgProof p -> countp current_size p
122 | Con.ArgMethod s -> (maxsize + 1)) in
123 let size = (countp 0 p) in
127 let is_big = is_big_general (Cexpr2pres.countterm)
131 let module Con = Content in
134 | `Hypothesis d -> d.Con.dec_id
135 | `Proof p -> p.Con.proof_id
136 | `Definition d -> d.Con.def_id
137 | `Joint jo -> jo.Con.joint_id
140 let make_row ?(attrs=[]) items concl =
141 let module P = Mpresentation in
143 P.Mtable _ -> (* big! *)
144 P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false";
145 None,"columnalign","left"],
146 [P.Mtr([],[P.Mtd ([],P.Mrow([],items))]);
147 P.Mtr ([],[P.Mtd ([],P.indented concl)])])
149 P.Mrow(attrs,items@[P.Mspace([None,"width","0.1cm"]);concl]))
152 let make_concl ?(attrs=[]) verb concl =
153 let module P = Mpresentation in
155 P.Mtable _ -> (* big! *)
156 P.Mtable (attrs@[None,"align","baseline 1"; None,"equalrows","false";
157 None,"columnalign","left"],
158 [P.Mtr([],[P.Mtd ([],P.Mtext([None,"mathcolor","Red"],verb))]);
159 P.Mtr ([],[P.Mtd ([],P.indented concl)])])
162 [P.Mtext([None,"mathcolor","Red"],verb);
163 P.Mspace([None,"width","0.1cm"]);
167 let make_args_for_apply term2pres args =
168 let module Con = Content in
169 let module P = Mpresentation in
170 let make_arg_for_apply is_first arg row =
173 Con.Aux n -> assert false
174 | Con.Premise prem ->
176 (match prem.Con.premise_binder with
181 P.Mi([],lemma.Con.lemma_name)::row
185 else P.Mi([],"_")::row
190 if is_first then res else P.smallskip::res
194 make_arg_for_apply true hd
195 (List.fold_right (make_arg_for_apply false) tl [])
199 let rec justification term2pres p =
200 let module Con = Content in
201 let module P = Mpresentation in
202 if ((p.Con.proof_conclude.Con.conclude_method = "Exact") or
203 ((p.Con.proof_context = []) &
204 (p.Con.proof_apply_context = []) &
205 (p.Con.proof_conclude.Con.conclude_method = "Apply"))) then
207 make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args in
209 P.Mtext([None,"mathcolor","Red"],"by")::P.Mspace([None,"width","0.1cm"])::
210 P.Mo([],"(")::pres_args@[P.Mo([],")")])
211 else proof2pres term2pres p
213 and proof2pres term2pres p =
214 let rec proof2pres p =
215 let module Con = Content in
216 let module P = Mpresentation in
221 | `Hypothesis _ -> true
223 ((List.filter is_decl p.Con.proof_context) != []) in
224 let omit_conclusion = (not indent) && (p.Con.proof_context != []) in
226 (match p.Con.proof_conclude.Con.conclude_conclusion with
228 | Some t -> Some (term2pres t)) in
231 conclude2pres p.Con.proof_conclude indent omit_conclusion in
233 acontext2pres p.Con.proof_apply_context presconclude indent in
234 context2pres p.Con.proof_context presacontext in
235 match p.Con.proof_name with
243 ([None,"actiontype","toggle" ; None,"selection","1"],
244 [P.Mtext [] "proof" ; body])
248 ([None,"actiontype","toggle" ; None,"selection","1"],
249 [(make_concl ~attrs:[Some "helm", "xref", p.Con.proof_id]
250 "proof of" ac); body])
252 P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
253 None,"columnalign","left"],
254 [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
255 P.Mtr ([],[P.Mtd ([], P.indented action)])])
257 P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
258 None,"columnalign","left";Some "helm", "xref", p.Con.proof_id],
259 [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
260 P.Mtr ([],[P.Mtd ([], P.indented action)])]) *)
262 and context2pres c continuation =
263 (* we generate a subtable for each context element, for selection
265 The table generated by the head-element does not have an xref;
266 the whole context-proof is already selectable *)
267 let module P = Mpresentation in
273 (fun ce continuation ->
274 let xref = get_xref ce in
275 P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
276 None,"columnalign","left"; Some "helm", "xref", xref ],
277 [P.Mtr([Some "helm", "xref", "ce_"^xref],[P.Mtd ([],ce2pres ce)]);
278 P.Mtr([],[P.Mtd ([], continuation)])])) tl continuation in
279 let hd_xref= get_xref hd in
280 P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
281 None,"columnalign","left"],
282 [P.Mtr([Some "helm", "xref", "ce_"^hd_xref],
283 [P.Mtd ([],ce2pres hd)]);
284 P.Mtr([],[P.Mtd ([], continuation')])])
287 let module P = Mpresentation in
288 let module Con = Content in
291 (match d.Con.dec_name with
293 let ty = term2pres d.Con.dec_type in
295 [P.Mtext([None,"mathcolor","Red"],"Assume");
296 P.Mspace([None,"width","0.1cm"]);
301 prerr_endline "NO NAME!!"; assert false)
303 (match h.Con.dec_name with
305 let ty = term2pres h.Con.dec_type in
307 [P.Mtext([None,"mathcolor","Red"],"Suppose");
308 P.Mspace([None,"width","0.1cm"]);
312 P.Mspace([None,"width","0.1cm"]);
315 prerr_endline "NO NAME!!"; assert false)
319 (match d.Con.def_name with
321 let term = term2pres d.Con.def_term in
328 prerr_endline "NO NAME!!"; assert false)
330 P.Mtext ([],"jointdef")
332 and acontext2pres ac continuation indent =
333 let module Con = Content in
334 let module P = Mpresentation in
336 (fun p continuation ->
339 P.indented (proof2pres p)
342 P.Mtable([None,"align","baseline 1"; None,"equalrows","false";
343 None,"columnalign","left"; Some "helm","xref",p.Con.proof_id],
344 [P.Mtr([Some "helm","xref","ace_"^p.Con.proof_id],[P.Mtd ([],hd)]);
345 P.Mtr([],[P.Mtd ([], continuation)])])) ac continuation
347 and conclude2pres conclude indent omit_conclusion =
348 let module Con = Content in
349 let module P = Mpresentation in
351 match conclude.Con.conclude_conclusion with
353 not omit_conclusion or
354 (* CSC: I ignore the omit_conclusion flag in this case. *)
355 (* CSC: Is this the correct behaviour? In the stylesheets *)
356 (* CSC: we simply generated nothing (i.e. the output type *)
357 (* CSC: of the function should become an option. *)
358 conclude.Con.conclude_method = "BU_Conversion" ->
359 let concl = (term2pres t) in
360 if conclude.Con.conclude_method = "BU_Conversion" then
361 make_concl "that is equivalent to" concl
362 else if conclude.Con.conclude_method = "FalseInd" then
363 (* false ind is in charge to add the conclusion *)
366 let conclude_body = conclude_aux conclude in
368 if conclude.Con.conclude_method = "TD_Conversion" then
369 make_concl "that is equivalent to" concl
370 else make_concl "we conclude" concl in
371 P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
372 None,"columnalign","left"],
373 [P.Mtr ([],[P.Mtd ([],conclude_body)]);
374 P.Mtr ([],[P.Mtd ([],ann_concl)])])
375 | _ -> conclude_aux conclude in
377 P.indented (P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],
380 P.Mrow ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
383 and conclude_aux conclude =
384 let module Con = Content in
385 let module P = Mpresentation in
386 if conclude.Con.conclude_method = "TD_Conversion" then
388 (match conclude.Con.conclude_conclusion with
389 None -> P.Mtext([],"NO EXPECTED!!!")
390 | Some c -> term2pres c) in
392 (match conclude.Con.conclude_args with
393 [Con.ArgProof p] -> p
394 | _ -> assert false) in
396 (match subproof.Con.proof_conclude.Con.conclude_conclusion with
397 None -> P.Mtext([],"NO SYNTH!!!")
398 | Some c -> (term2pres c)) in
400 ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
401 [P.Mtr([],[P.Mtd([],make_concl "we must prove" expected)]);
402 P.Mtr([],[P.Mtd([],make_concl "or equivalently" synth)]);
403 P.Mtr([],[P.Mtd([],proof2pres subproof)])])
404 else if conclude.Con.conclude_method = "BU_Conversion" then
406 else if conclude.Con.conclude_method = "Exact" then
408 (match conclude.Con.conclude_args with
409 [Con.Term t] -> term2pres t
410 | _ -> assert false) in
411 (match conclude.Con.conclude_conclusion with
414 [p_mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
415 | Some c -> let conclusion = term2pres c in
417 [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")]
420 else if conclude.Con.conclude_method = "Intros+LetTac" then
421 (match conclude.Con.conclude_args with
422 [Con.ArgProof p] -> proof2pres p
426 (match conclude.Con.conclude_conclusion with
427 None -> P.Mtext([],"NO Conclusion!!!")
428 | Some c -> term2pres c) in
429 (match conclude.Con.conclude_args with
432 ([None,"align","baseline 1"; None,"equalrows","false";
433 None,"columnalign","left"],
434 [P.Mtr([],[P.Mtd([],proof2pres p)]);
436 (make_concl "we proved 1" conclusion))])]);
439 else if (conclude.Con.conclude_method = "ByInduction") then
441 else if (conclude.Con.conclude_method = "Exists") then
443 else if (conclude.Con.conclude_method = "AndInd") then
445 else if (conclude.Con.conclude_method = "FalseInd") then
447 else if (conclude.Con.conclude_method = "Rewrite") then
449 (match (List.nth conclude.Con.conclude_args 6) with
450 Con.ArgProof p -> justification term2pres p
451 | _ -> assert false) in
453 (match List.nth conclude.Con.conclude_args 2 with
454 Con.Term t -> term2pres t
455 | _ -> assert false) in
457 (match List.nth conclude.Con.conclude_args 5 with
458 Con.Term t -> term2pres t
459 | _ -> assert false) in
460 P.Mtable ([None,"align","baseline 1";None,"equalrows","false";
461 None,"columnalign","left"],
462 [P.Mtr ([],[P.Mtd ([],P.Mrow([],[
463 P.Mtext([None,"mathcolor","Red"],"rewrite");
464 P.Mspace([None,"width","0.1cm"]);term1;
465 P.Mspace([None,"width","0.1cm"]);
466 P.Mtext([None,"mathcolor","Red"],"with");
467 P.Mspace([None,"width","0.1cm"]);term2]))]);
468 P.Mtr ([],[P.Mtd ([],P.indented justif)])]);
469 else if conclude.Con.conclude_method = "Apply" then
471 make_args_for_apply term2pres conclude.Con.conclude_args in
473 P.Mtext([None,"mathcolor","Red"],"by")::
474 P.Mspace([None,"width","0.1cm"])::
475 P.Mo([],"(")::pres_args@[P.Mo([],")")])
478 ([None,"align","baseline 1"; None,"equalrows","false"; None,"columnalign","left"],
479 [P.Mtr ([],[P.Mtd ([],P.Mtext([],"Apply method" ^ conclude.Con.conclude_method ^ " to"))]);
484 ([None,"align","baseline 1"; None,"equalrows","false";
485 None,"columnalign","left"],
486 args2pres conclude.Con.conclude_args))))])])
489 let module P = Mpresentation in
491 (function a -> P.Mtr ([], [P.Mtd ([], arg2pres a)])) l
494 let module P = Mpresentation in
495 let module Con = Content in
498 P.Mtext ([],"aux " ^ n)
499 | Con.Premise prem ->
500 P.Mtext ([],"premise")
508 P.Mtext ([],"method")
510 and byinduction conclude =
511 let module P = Mpresentation in
512 let module Con = Content in
513 let proof_conclusion =
514 (match conclude.Con.conclude_conclusion with
515 None -> P.Mtext([],"No conclusion???")
516 | Some t -> term2pres t) in
517 let inductive_arg,args_for_cases =
518 (match conclude.Con.conclude_args with
520 let l1,l2 = split (int_of_string n) tl in
521 let last_pos = (List.length l2)-1 in
522 List.nth l2 last_pos,l1
523 | _ -> assert false) in
526 (match inductive_arg with
528 P.Mtext ([],"an aux???")
529 | Con.Premise prem ->
530 (match prem.Con.premise_binder with
531 None -> P.Mtext ([],"the previous result")
532 | Some n -> P.Mi([],n))
533 | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name)
537 P.Mtext ([],"a proof???")
539 P.Mtext ([],"a method???")) in
540 (make_concl "we proceede by induction on" arg) in
542 (make_concl "to prove" proof_conclusion) in
544 ([None,"align","baseline 1"; None,"equalrows","false";
545 None,"columnalign","left"],
546 P.Mtr ([],[P.Mtd ([],induction_on)])::
547 P.Mtr ([],[P.Mtd ([],to_prove)])::
548 (make_cases args_for_cases))
550 and make_cases args_for_cases =
551 let module P = Mpresentation in
553 (fun p -> P.Mtr ([],[P.Mtd ([],make_case p)])) args_for_cases
556 let module P = Mpresentation in
557 let module Con = Content in
561 (match p.Con.proof_name with
562 None -> P.Mtext([],"no name for case!!")
563 | Some n -> P.Mi([],n)) in
567 `Hypothesis h -> h.Con.dec_inductive
568 | _ -> false) p.Con.proof_context in
577 (match h.Con.dec_name with
580 [P.Mspace([None,"width","0.1cm"]);
583 (term2pres h.Con.dec_type)]
584 | _ -> [P.Mtext ([],"???")]) in
587 P.Mtr ([],[P.Mtd ([],P.Mrow([],
588 P.Mtext([],"Case")::P.Mspace([None,"width","0.1cm"])::name::pattern_aux@
589 [P.Mspace([None,"width","0.1cm"]);
590 P.Mtext([],"->")]))]) in
592 (match p.Con.proof_conclude.Con.conclude_conclusion with
593 None -> P.Mtext([],"No conclusion!!!")
594 | Some t -> term2pres t) in
597 P.indented (make_concl "the thesis becomes" subconcl))]) in
598 let induction_hypothesis =
603 P.Mtr([],[P.Mtd([], P.indented
604 (P.Mtext([],"by induction hypothesis we know:")))]) in
609 (match h.Con.dec_name with
612 P.indented (P.Mrow ([],
616 P.Mspace([None,"width","0.1cm"]);
617 term2pres h.Con.dec_type]))
618 | _ -> assert false in
621 (function ce -> P.Mtr ([], [P.Mtd ([], make_hyp ce)]))
625 acontext2pres_old p.Con.proof_apply_context true in *)
626 let body = conclude2pres p.Con.proof_conclude true false in
629 match p.Con.proof_apply_context with
630 [] -> p.Con.proof_conclude.Con.conclude_id
631 | {Con.proof_id = id}::_ -> id
633 P.Maction([None,"actiontype","toggle" ; None,"selection","1"],
636 ([None,"mathcolor","Red" ;
637 Some "helm", "xref", acontext_id],"Proof")) ;
638 acontext2pres p.Con.proof_apply_context body true]) in
639 P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
640 None,"columnalign","left"],
641 pattern::asubconcl::induction_hypothesis@
642 [P.Mtr([],[P.Mtd([],presacontext)])])
645 and falseind conclude =
646 let module P = Mpresentation in
647 let module Con = Content in
648 let proof_conclusion =
649 (match conclude.Con.conclude_conclusion with
650 None -> P.Mtext([],"No conclusion???")
651 | Some t -> term2pres t) in
653 (match conclude.Con.conclude_args with
654 [Con.Aux(n);_;case_arg] -> case_arg
657 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
661 Con.Aux n -> assert false
662 | Con.Premise prem ->
663 (match prem.Con.premise_binder with
664 None -> [P.Mtext([],"Contradiction, hence")]
666 [P.Mi([],n);P.smallskip;P.Mtext([],"is contradictory, hence")])
668 [P.Mi([],lemma.Con.lemma_name);P.smallskip;P.Mtext([],"is contradictory, hence")]
669 | _ -> assert false) in
670 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
671 make_row arg proof_conclusion
673 and andind conclude =
674 let module P = Mpresentation in
675 let module Con = Content in
676 let proof_conclusion =
677 (match conclude.Con.conclude_conclusion with
678 None -> P.Mtext([],"No conclusion???")
679 | Some t -> term2pres t) in
681 (match conclude.Con.conclude_args with
682 [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
685 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
689 Con.Aux n -> assert false
690 | Con.Premise prem ->
691 (match prem.Con.premise_binder with
693 | Some n -> [P.Mtext([],"by");P.smallskip;P.Mi([],n)])
695 [P.Mtext([],"by");P.smallskip;P.Mi([],lemma.Con.lemma_name)]
696 | _ -> assert false) in
697 match proof.Con.proof_context with
698 `Hypothesis hyp1::`Hypothesis hyp2::tl ->
700 (match hyp.Con.dec_name with
706 P.Mi([],get_name hyp1);
709 term2pres hyp1.Con.dec_type]) in
713 P.Mi([],get_name hyp2);
716 term2pres hyp2.Con.dec_type]) in
717 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
718 let body = conclude2pres proof.Con.proof_conclude false true in
720 acontext2pres proof.Con.proof_apply_context body false in
722 ([None,"align","baseline 1"; None,"equalrows","false";
723 None,"columnalign","left"],
724 [P.Mtr ([],[P.Mtd ([],
725 P.Mrow([],arg@[P.smallskip;P.Mtext([],"we have")]))]);
726 P.Mtr ([],[P.Mtd ([],preshyp1)]);
727 P.Mtr ([],[P.Mtd ([],P.Mtext([],"and"))]);
728 P.Mtr ([],[P.Mtd ([],preshyp2)]);
729 P.Mtr ([],[P.Mtd ([],presacontext)])]);
732 and exists conclude =
733 let module P = Mpresentation in
734 let module Con = Content in
735 let proof_conclusion =
736 (match conclude.Con.conclude_conclusion with
737 None -> P.Mtext([],"No conclusion???")
738 | Some t -> term2pres t) in
740 (match conclude.Con.conclude_args with
741 [Con.Aux(n);_;Con.ArgProof proof;_] -> proof
744 List.map (ContentPp.parg 0) conclude.Con.conclude_args;
746 match proof.Con.proof_context with
747 `Declaration decl::`Hypothesis hyp::tl
748 | `Hypothesis decl::`Hypothesis hyp::tl ->
750 (match decl.Con.dec_name with
755 [P.Mtext([None,"mathcolor","Red"],"let");
757 P.Mi([],get_name decl);
758 P.Mtext([],":"); term2pres decl.Con.dec_type]) in
761 [P.Mtext([None,"mathcolor","Red"],"such that");
764 P.Mi([],get_name hyp);
767 term2pres hyp.Con.dec_type]) in
768 (* let body = proof2pres {proof with Con.proof_context = tl} in *)
769 let body = conclude2pres proof.Con.proof_conclude false true in
771 acontext2pres proof.Con.proof_apply_context body false in
773 ([None,"align","baseline 1"; None,"equalrows","false";
774 None,"columnalign","left"],
775 [P.Mtr ([],[P.Mtd ([],presdecl)]);
776 P.Mtr ([],[P.Mtd ([],suchthat)]);
777 P.Mtr ([],[P.Mtd ([],presacontext)])]);
778 | _ -> assert false in
785 let content2pres term2pres (id,params,metasenv,obj) =
786 let module K = Content in
787 let module P = Mpresentation in
789 `Def (K.Const,thesis,`Proof p) ->
791 [None,"align","baseline 1";
792 None,"equalrows","false";
793 None,"columnalign","left";
794 None,"helm:xref","id"]
799 ("UNFINISHED PROOF" ^ id ^"(" ^
800 String.concat " ; " (List.map UriManager.string_of_uri params)^
805 [p_mtext [] "THESIS:"])] ;
811 term2pres thesis])]] @
817 (* Conjectures are in their own table to make *)
818 (* diffing the DOM trees easier. *)
820 [None,"align","baseline 1";
821 None,"equalrows","false";
822 None,"columnalign","left"]
826 [p_mtext [] "CONJECTURES:"])])::
832 (p_mrow [Some "helm", "xref", id]
840 | Some (`Declaration d)
841 | Some (`Hypothesis d) ->
843 { K.dec_name = dec_name ;
844 K.dec_type = ty } = d
853 | Some (`Definition d) ->
855 { K.def_name = def_name ;
856 K.def_term = bo } = d
866 let proof_name = p.K.proof_name in
869 (match proof_name with
873 proof2pres term2pres p]
874 ) (List.rev context) @
876 [ p_mi [] (string_of_int n) ;
887 [proof2pres term2pres p])]])
891 let content2pres ~ids_to_inner_sorts =
894 (Cexpr2pres.cexpr2pres_charcount
895 (Content_expressions.acic2cexpr ids_to_inner_sorts p)))