From 99727f61d0a718e34d4282f9b9b45fce4336af84 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Jul 2007 20:15:18 +0000
Subject: [PATCH] is_top_down was not propageted correctly under a bottom-up
 conversion.

---
 .../components/content_pres/content2pres.ml   | 41 +++++++++----------
 1 file changed, 20 insertions(+), 21 deletions(-)

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index 7d4839e03..ae7c8d46d 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -136,7 +136,7 @@ let rec justification term2pres p =
     Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)])
      
 and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
-  let rec proof2pres ?skip_initial_lambdas_internal is_top_down p omit_dot =
+  let rec proof2pres ?skip_initial_lambdas_internal is_top_down p in_bu_conversion =
     let indent = 
       let is_decl e = 
         (match e with 
@@ -152,18 +152,20 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
     let body =
         let presconclude = 
           conclude2pres
-           ?skip_initial_lambdas_internal:
-             (match skip_initial_lambdas_internal with
-                 Some (`Later s) -> Some (`Now s)
-               | _ -> None)
-             is_top_down
-             p.Con.proof_name p.Con.proof_conclude indent omit_conclusion
-           omit_dot in
+          ?skip_initial_lambdas_internal:
+            (match skip_initial_lambdas_internal with
+                Some (`Later s) -> Some (`Now s)
+              | _ -> None)
+          is_top_down p.Con.proof_name p.Con.proof_conclude indent
+          omit_conclusion in_bu_conversion in
         let presacontext = 
           acontext2pres
-           (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
-            p.Con.proof_apply_context
-            presconclude indent
+           (if p.Con.proof_conclude.Con.conclude_method = "BU_Conversion" then
+             is_top_down
+            else
+             false)
+           p.Con.proof_apply_context
+           presconclude indent
            (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
         in
         context2pres 
@@ -172,6 +174,7 @@ 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 ->
@@ -277,18 +280,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
             [] -> in_bu_conversion
           | p::_ -> p.Con.proof_conclude.Con.conclude_method = "BU_Conversion"
         in
-        let hd = 
-          if indent then
-            B.indent (proof2pres is_top_down p in_bu_conversion)
-          else 
-            proof2pres is_top_down p in_bu_conversion
-        in
-        B.V([Some "helm","xref",p.Con.proof_id],
+        let hd = proof2pres is_top_down p in_bu_conversion in
+        let hd = if indent then B.indent hd else hd in
+         B.V([Some "helm","xref",p.Con.proof_id],
           [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
            continuation])
    in aux ac
 
-  and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion omit_dot =
+  and conclude2pres ?skip_initial_lambdas_internal is_top_down name conclude indent omit_conclusion in_bu_conversion =
     let tconclude_body = 
       match conclude.Con.conclude_conclusion with
         Some t (*when not omit_conclusion or
@@ -342,14 +341,14 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
                 B.H([], [B.b_kw "done" ; B.Text([],".") ])
               else
                 B.b_hv []
-                 ((if not is_top_down || omit_dot then
+                 ((if not is_top_down || in_bu_conversion then
                     (make_concl "we proved" concl) ::
                       if not is_top_down then
                        let name = get_name ~default:"previous" name in
                         [B.b_space; B.Text([],"(" ^ name ^ ")")]
                       else []
                    else [B.b_kw "done"]
-                  ) @ if not omit_dot then [B.Text([],".")] else [])
+                  ) @ if not in_bu_conversion then [B.Text([],".")] else [])
             in
              B.V ([], prequel @ [conclude_body; ann_concl])
       | _ -> conclude_aux ?skip_initial_lambdas_internal is_top_down conclude
-- 
2.39.2