X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2Fcontent2pres.ml;h=018497404cf3277aef6f93c9636d07825eb8b427;hb=cd99db7e082123b0e410d65f364f340aeb1af3d7;hp=a41ccc99158a73562218887d2d786e57d903121e;hpb=4ed827ab0c5a05ff3b496810d73d9f584e9dac3e;p=helm.git

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index a41ccc991..018497404 100644
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -290,11 +290,8 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
           else  
             let prequel =
               if
-               (match skip_initial_lambdas_internal with
-                   None
-                 | Some (`Later _) -> true
-                 | Some (`Now _) -> false)
-               && conclude.Con.conclude_method = "Intros+LetTac"
+               (not is_top_down) &&
+                conclude.Con.conclude_method = "Intros+LetTac"
               then
                 let name = get_name name in
                  [B.V ([],