From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 30 Jun 2007 12:10:09 +0000 (+0000)
Subject: Spurious "we need to prove" at the beginning of Intros+LetTac are no longer
X-Git-Tag: make_still_working~6232
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cd99db7e082123b0e410d65f364f340aeb1af3d7;p=helm.git

Spurious "we need to prove" at the beginning of Intros+LetTac are no longer
generated.
---

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 ([],