fixed Whelp stuff

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

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index ef79ab4ad254aebac239a96dbf31f83281565e59..fdffe82760b840622a2f33829903e7d13abee456 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -261,7 +261,7 @@ and proof2pres term2pres p =
              [B.H([Some "helm", "xref", "ce_"^hd_xref],
                [ce2pres hd]);
              continuation'])
-         
+        
   and ce2pres =
     let module Con = Content in
       function
@@ -304,8 +304,10 @@ and proof2pres term2pres p =
                    term])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | `Joint ho -> 
-            B.Text ([],"jointdef")
+      | `Joint ho -> assert false (*
+        B.H ([],
+        (B.Text ([],"JOINT ")
+        :: List.map ce2pres ho.Content.joint_defs)) *)
 
   and acontext2pres ac continuation indent =
     let module Con = Content in
@@ -380,7 +382,11 @@ and proof2pres term2pres p =
       let arg = 
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
-         | _ -> assert false) in
+         | [Con.Premise p] -> 
+             (match p.Con.premise_binder with
+             | None -> assert false; (* unnamed hypothesis ??? *)
+             | Some s -> B.Text([],s))
+         | err -> assert false) in
       (match conclude.Con.conclude_conclusion with 
          None ->
           B.b_h [] [B.b_kw "Consider"; B.b_space; arg]