Dead code removed.

[helm.git] / helm / ocaml / content_pres / content2pres.ml

diff --git a/helm/ocaml/content_pres/content2pres.ml b/helm/ocaml/content_pres/content2pres.ml
index 195ce0f77b1cf9b2a3008623517c7c364a16442b..948eb7b9ac7c58293123397cc150de0f4705349a 100644 (file)
--- 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