Added initial support for inversion principles in Matita NG.

[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 9c389467c1f6cef38b4bd03536040ed599024033..c88f87535f71fe71aa6aac2e539060ad8cea7ae6 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -136,7 +136,8 @@ let rec justification ~for_rewriting_step ~ignore_atoms term2pres p =
       make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
     in
      [B.H([],
-       (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+     (*(if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::*)
+       (B.b_kw "by")::
        B.b_space::
        B.Text([],"(")::pres_args@[B.Text([],")")])], None 
   else