From 15c68b7390bae4e2d228056378f882764812b090 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 31 Jul 2007 10:39:31 +0000 Subject: [PATCH 1/1] removed comments in proof presentation --- helm/software/components/content_pres/content2pres.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml index a99278dbc..e25ff40d8 100644 --- a/helm/software/components/content_pres/content2pres.ml +++ b/helm/software/components/content_pres/content2pres.ml @@ -181,7 +181,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p = | _ -> p.Con.proof_context) presacontext in +(* let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in +*) match p.Con.proof_name with None -> body | Some name -> -- 2.39.2