changed auto_tac params type and all derivate tactics like applyS and

[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 b9e89769472371c31b3a27e4ae8beedf1db53c49..228b6fdeb0cc73c6c08efabc0b618800f6e4976f 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -121,7 +121,7 @@ let add_xref id = function
   | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t)
   | _ -> assert false (* TODO, add_xref is meaningful for all boxes *)
 
-let rec justification ~ignore_atoms term2pres p = 
+let rec justification ~for_rewriting_step ~ignore_atoms term2pres p = 
   if p.Con.proof_conclude.Con.conclude_method = "Exact" &&
      ignore_atoms
   then
@@ -136,10 +136,16 @@ let rec justification ~ignore_atoms term2pres p =
       make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
     in
      [B.H([],
-       (B.b_kw "by")::B.b_space::
+       (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+       B.b_space::
        B.Text([],"(")::pres_args@[B.Text([],")")])], None 
   else
-   [B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"])],
+   [B.H([],
+    if for_rewriting_step then
+     [B.b_kw "proof"]
+    else
+     [B.b_kw "by"; B.b_space; B.b_kw "proof"]
+    )],
     Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)])
      
 and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
@@ -441,7 +447,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
          || conclude.Con.conclude_method = "RewriteRL" then
       let justif1,justif2 = 
         (match (List.nth conclude.Con.conclude_args 6) with
-           Con.ArgProof p -> justification ~ignore_atoms:true term2pres p
+           Con.ArgProof p ->
+            justification ~for_rewriting_step:true ~ignore_atoms:true
+             term2pres p
          | _ -> assert false) in
       let justif =
        match justif2 with
@@ -483,7 +491,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
       B.V([], justif @ [B.b_kw "by _"])
     else if conclude.Con.conclude_method = "Eq_chain" then
       let justification p =
-       let j1,j2 = justification ~ignore_atoms:false term2pres p in
+       let j1,j2 =
+        justification ~for_rewriting_step:true ~ignore_atoms:false term2pres p
+       in
         j1, match j2 with Some j -> [j] | None -> []
       in
       let rec aux args =