Bug fixed: RewriteLR were not recognized correctly. Moreover they were also

[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 24c4faa348aa4e1c853b75ff5b5a79ae0b0cec5d..477697580fd4df83314ad345634a798b47870237 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
@@ -502,8 +502,14 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
          | Con.Term (_,t) -> t 
          | _ -> assert false 
       in
-      B.HOV([],[B.b_kw "conclude";B.b_space;term2pres hd; (* B.b_space; *)
-             B.V ([],aux (List.tl conclude.Con.conclude_args))])
+       if is_top_down then
+        B.HOV([],
+         [B.b_kw "conclude";B.b_space;term2pres hd;
+         B.V ([],aux (List.tl conclude.Con.conclude_args))])
+       else
+        B.HOV([],
+         [B.b_kw "obtain";B.b_space;B.b_kw "FIXMEXX"; B.b_space;term2pres hd;
+         B.V ([],aux (List.tl conclude.Con.conclude_args))])
     else if conclude.Con.conclude_method = "Apply" then
       let pres_args = 
         make_args_for_apply term2pres conclude.Con.conclude_args in