From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Jan 2006 12:04:07 +0000 (+0000)
Subject: Dead code removed.
X-Git-Tag: make_still_working~7858
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=339af4cc4fb745a8b284bde75b36178a26055468;p=helm.git

Dead code removed.
---

diff --git a/helm/ocaml/content_pres/content2pres.ml b/helm/ocaml/content_pres/content2pres.ml
index 195ce0f77..948eb7b9a 100644
--- a/helm/ocaml/content_pres/content2pres.ml
+++ b/helm/ocaml/content_pres/content2pres.ml
@@ -565,10 +565,6 @@ and proof2pres term2pres p =
        make_row arg proof_conclusion
 
      and andind conclude =
-       let proof_conclusion = 
-         (match conclude.Con.conclude_conclusion with
-            None -> B.b_kw "No conclusion???"
-          | Some t -> term2pres t) in
        let proof,case_arg = 
          (match conclude.Con.conclude_args with
              [Con.Aux(n);_;Con.ArgProof proof;case_arg] -> proof,case_arg
@@ -621,10 +617,6 @@ and proof2pres term2pres p =
          | _ -> assert false
 
      and exists conclude =
-       let proof_conclusion = 
-         (match conclude.Con.conclude_conclusion with
-            None -> B.b_kw "No conclusion???"
-          | Some t -> term2pres t) in
        let proof = 
          (match conclude.Con.conclude_args with
              [Con.Aux(n);_;Con.ArgProof proof;_] -> proof