Back-ported to camlp5 < 5.00.

[helm.git] / helm / software / components / content_pres / content2pres.ml

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index a99278dbcf137de171eff09cb3f5339fde9b8ab7..b9e89769472371c31b3a27e4ae8beedf1db53c49 100644 (file)
--- 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 ->
@@ -447,9 +449,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
         | Some j -> [j]
       in
       let index_term1, index_term2 =
-       if  (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
-        || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down)
-       then 2,5 else 5,2
+       if conclude.Con.conclude_method = "RewriteLR" then 2,5 else 5,2
       in
       let term1 = 
         (match List.nth conclude.Con.conclude_args index_term1 with
@@ -960,7 +960,7 @@ let content2pres
   content2pres ?skip_initial_lambdas ?skip_thm_and_qed
     (fun ?(prec=90) annterm ->
       let ast, ids_to_uris =
-        TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+       TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
       in
        CicNotationPres.box_of_mpres
         (CicNotationPres.render ids_to_uris ~prec